Andrej Bauer

Generating author description...

All published works

Action	Title	Year	Authors
+	Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem	2025	Andrej Bauer
+ PDF Chat	Comodule Representations of Second-Order Functionals	2024	Danel Ahman Andrej Bauer
+ PDF Chat	An Imperative Language for Verified Exact Real-Number Computation	2024	Andrej Bauer Sewon Park Alex Simpson
+ PDF Chat	The Countable Reals	2024	Andrej Bauer James Hanson
+ PDF Chat	Finitary Type Theories With and Without Contexts	2023	Philipp G. Haselwarter Andrej Bauer
+	Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem	2023	Andrej Bauer
+	MLFMF: Data Sets for Machine Learning for Mathematical Formalization	2023	Andrej Bauer Matej Petković Ljupčo Todorovski
+ PDF Chat	Instance reducibility and Weihrauch degrees	2022	Andrej Bauer
+ PDF Chat	An extensible equality checking algorithm for dependent type theories	2022	Andrej Bauer Anja Petković Komel
+ PDF Chat	Finitary type theories with and without contexts	2021	Philipp G. Haselwarter Andrej Bauer
+	Instance reducibility and Weihrauch degrees	2021	Andrej Bauer
+	Finitary type theories with and without contexts	2021	Philipp G. Haselwarter Andrej Bauer
+	A general definition of dependent type theories	2020	Andrej Bauer Philipp G. Haselwarter Peter LeFanu Lumsdaine
+	Runners in Action	2020	Danel Ahman Andrej Bauer
+	Every metric space is separable in function realizability	2019	Andrej Bauer Andrew Swan
+	What is algebraic about algebraic effects and handlers	2018	Andrej Bauer
+	Design and Implementation of the Andromeda Proof Assistant	2018	Andrej Bauer Gaëtan Gilbert Philipp G. Haselwarter Matija Pretnar C. Addison Stone
+	Every metric space is separable in function realizability	2018	Andrej Bauer Andrew Swan
+	Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341).	2018	Andrej Bauer Martı́n Hötzel Escardó Peter LeFanu Lumsdaine Assia Mahboubi
+	What is algebraic about algebraic effects and handlers?	2018	Andrej Bauer
+	The HoTT library: a formalization of homotopy type theory in Coq	2016	Andrej Bauer Jason Gross Peter LeFanu Lumsdaine Michael Shulman Matthieu Sozeau Bas Spitters
+	The HoTT Library: A formalization of homotopy type theory in Coq	2016	Andrej Bauer Jason Gross Peter LeFanu Lumsdaine Mike Shulman Matthieu Sozeau Bas Spitters
+	The HoTT Library: A formalization of homotopy type theory in Coq	2016	Andrej Bauer Jason N. Gross Peter LeFanu Lumsdaine Mike Shulman Matthieu Sozeau Bas Spitters
+	Mathematics of the Transcendental—A Book Review by Andrej Bauer	2015	Andrej Bauer
+	Mathematics of the Transcendental—A Book Review by	2015	Andrej Bauer
+ PDF Chat	An Effect System for Algebraic Effects and Handlers	2014	Andrej Bauer Matija Pretnar
+	An injection from the Baire space to natural numbers	2014	Andrej Bauer
+ PDF Chat	Programming with algebraic effects and handlers	2014	Andrej Bauer Matija Pretnar
+	Cartesian closed categories of separable Scott domains	2014	Andrej Bauer Gordon Plotkin Dana Scott
+	Stone Duality for Skew Boolean Algebras with Intersections	2013	Andrej Bauer Karin Cvetko-Vah
+ PDF Chat	A non-commutative Priestley duality	2013	Andrej Bauer Karin Cvetko-Vah Mai Gehrke Samuel J. van Gool Ganna Kudryavtseva
+ PDF Chat	On the Bourbaki–Witt principle in toposes	2013	Andrej Bauer Peter LeFanu Lumsdaine
+ PDF Chat	An Effect System for Algebraic Effects and Handlers	2013	Andrej Bauer Matija Pretnar
+	Homotopy Type Theory: Univalent Foundations of Mathematics	2013	Peter Aczel Benedikt Ahrens Thorsten Altenkirch Steve Awodey Bruno Barras Andrej Bauer Yves Bertot Marc Bezem Thierry Coquand Eric Finster
+	Intuitionistic Mathematics and Realizability in the Physical World	2012	Andrej Bauer
+	A non-commutative Priestley duality	2012	Andrej Bauer Karin Cvetko-Vah Mai Gehrke Sam van Gool Ganna Kudryavtseva
+	A non-commutative Priestley duality	2012	Andrej Bauer Karin Cvetko-Vah Mai Gehrke Sam van Gool Ganna Kudryavtseva
+	On the failure of fixed-point theorems for chain-complete lattices in the effective topos	2011	Andrej Bauer
+	Metric spaces in synthetic topology	2011	Andrej Bauer Davorin Lešnik
+	Stone Duality for Skew Boolean Algebras with Intersections	2011	Andrej Bauer Karin Cvetko-Vah
+	An injection from N N to N	2011	Andrej Bauer
+	On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos	2009	Andrej Bauer
+	The Dedekind Reals in Abstract Stone Duality.	2005	Andrej Bauer Paul Taylor
+	Two constructive embedding‐extension theorems with applications to continuity principles and to Banach‐Mazur computability	2004	Andrej Bauer Alex Simpson
+	Locally Non-compact Spaces and Continuity Rinciples	2003	Alexander Simpson Andrej Bauer
+	A Relationship between Equilogical Spaces and Type Two Effectivity	2001	Andrej Bauer
+	The realizability approach to computable analysis and topology	2000	Andrej Bauer Dana Scott
+	Continuous Functionals of Dependent Types and Equilogical Spaces	2000	Andrej Bauer Lars Birkedal
+	Multibasic and Mixed Hypergeometric Gosper-Type Algorithms	1999	Andrej Bauer Marko Petkovšek
+	Analytica — An experiment in combining theorem proving and symbolic computation	1996	Andrej Bauer Edmund Clarke Xudong Zhao

Common Coauthors

Coauthor	Papers Together
Peter LeFanu Lumsdaine	7
Philipp G. Haselwarter	5
Karin Cvetko-Vah	5
Matthieu Sozeau	4
Matija Pretnar	4
Bas Spitters	4
Dana Scott	3
Mai Gehrke	3
Ganna Kudryavtseva	3
Assia Mahboubi	2
Jason Gross	2
Danel Ahman	2
Martı́n Hötzel Escardó	2
Andrew Swan	2
Michael Shulman	2
Sam van Gool	2
Joachim Koch	1
James Hanson	1
Anthony Bordg	1
Andrew Polonsky	1
Sergey A. Melikhov	1
Matej Petković	1
Benno van den Berg	1
Alexander Simpson	1
Erik Palmgren	1
Davorin Lešnik	1
Richard Garner	1
Mike Shulman	1
Steve Awodey	1
Nicola Gambino	1
Peter Aczel	1
Paul Taylor	1
Peter Dybjer	1
Lars Birkedal	1
Thorsten Altenkirch	1
Samuel J. van Gool	1
Ljupčo Todorovski	1
Michael Nahas	1
Vladimir Voevodsky	1
Hugo Herbelin	1
Philip Scott	1
Kuen-Bang Hou	1
Mike Shulman	1
Marko Petkovšek	1
Álvaro Pelayo	1
C. Addison Stone	1
Gordon Plotkin	1
André Joyal	1
Georges Gonthier	1
Guillaume Brunerie	1

Commonly Cited References

Action	Title	Year	Authors	# of times referenced
+	The realizability approach to computable analysis and topology	2000	Andrej Bauer Dana Scott	6
+	Sheaves in Geometry and Logic: A First Introduction to Topos Theory	2018	Saunders MacLane Galdós Ieke Moerdijk	6
+	None	2003	Gordon Plotkin John Power	5
+ PDF Chat	Quantum Gauge Field Theory in Cohesive Homotopy Type Theory	2014	Urs Schreiber Michael Shulman	5
+	Tensors of Comodels and Models for Operational Semantics	2008	Gordon Plotkin John Power	4
+	Skew lattices in rings	1989	Jonathan Leech	4
+ PDF Chat	Programming with algebraic effects and handlers	2014	Andrej Bauer Matija Pretnar	4
+ PDF Chat	Cubical Type Theory: a constructive interpretation of the univalence axiom	2015	Cyril Cohen Thierry Coquand Simon Huber Anders Mörtberg	3
+	Categories of domains with totality	1997	Dag Normann	3
+ PDF Chat	Infinite time Turing machines	2000	Joel David Hamkins Andy Lewis	3
+	Diagonal arguments and cartesian closed categories	1969	F. William Lawvere	3
+	Sheaves in Geometry and Logic	1994	Saunders Mac Lane Ieke Moerdijk	3
+	Continuous Functionals of Dependent Types and Equilogical Spaces	2000	Andrej Bauer Lars Birkedal	3
+	Modelling environments in call-by-value programming languages	2003	Paul Blain Levy John Power Hayo Thielecke	3
+	Beweisstudien zum Satz von M. Zorn. Herrn Erhard. Schmidt zum 75. Geburtstag gewidmet	1950	Ernst Witt	3
+	Sur le théorème de Zorn	1949	Nicolás Bourbaki	3
+	Experimental library of univalent formalization of mathematics	2014	Vladimir Voevodsky	2
+ PDF Chat	Univalence for inverse diagrams and homotopy canonicity	2014	Michael Shulman	2
+ PDF Chat	Homotopy theoretic models of identity types	2008	Steve Awodey Michael A. Warren	2
+ PDF Chat	A DUALIZING OBJECT APPROACH TO NONCOMMUTATIVE STONE DUALITY	2013	Ganna Kudryavtseva	2
+	A general definition of dependent type theories	2020	Andrej Bauer Philipp G. Haselwarter Peter LeFanu Lumsdaine	2
+ PDF Chat	Topological and limit-space subcategories of countably-based equilogical spaces	2002	Matı́as Menni Alex Simpson	2
+ PDF Chat	The Categories of Boolean Lattices, Boolean Rings and Boolean Spaces	1964	Hoshang Pesotan Doctor	2
+ PDF Chat	A refinement of Stone duality to skew Boolean algebras	2012	Ganna Kudryavtseva	2
+	Algebraic Presentations of Dependent Type Theories	2016	Valery Isaev	2
+ PDF Chat	An Effect System for Algebraic Effects and Handlers	2014	Andrej Bauer Matija Pretnar	2
+	From Comodels to Coalgebras: State and Arrays	2004	John Power Olha Shkaravska	2
+ PDF Chat	Prime ideal structure in commutative rings	1969	M. Hochster	2
+ PDF Chat	Categories for the Working Mathematician	1971	Saunders Mac Lane	2
+ PDF Chat	NON-COMMUTATIVE STONE DUALITY: INVERSE SEMIGROUPS, TOPOLOGICAL GROUPOIDS AND C*-ALGEBRAS	2012	Mark V. Lawson	2
+ PDF Chat	Univalent categories and the Rezk completion	2015	Benedikt Ahrens Krzysztof Kapulkin Michael Shulman	2
+	Non-standard analysis	1966	Abraham Robinson	2
+	Pseudogroups and their étale groupoids	2013	Mark V. Lawson Daniel Lenz	2
+ PDF Chat	Representation theory of MV-algebras	2010	Eduardo J. Dubuc Yuri A. Poveda	2
+ PDF Chat	Type classes for efficient exact real arithmetic in Coq	2013	Robbert Krebbers Bas Spitters	2
+ PDF Chat	Applications of the theory of Boolean rings to general topology	1937	M. H. Stone	2
+ PDF Chat	In Domain Realizability, not all Functionals on C[–1, 1] are Continuous	2002	Martı́n Hötzel Escardó Thomas Streicher	2
+	Partial Horn logic and cartesian categories	2006	Erik Palmgren Steve Vickers	2
+	A dualizing object approach to non-commutative Stone duality	2011	Ganna Kudryavtseva	2
+ PDF Chat	A NONCOMMUTATIVE GENERALIZATION OF STONE DUALITY	2010	Mark V. Lawson	2
+	Stone Duality for Skew Boolean Algebras with Intersections	2013	Andrej Bauer Karin Cvetko-Vah	2
+ PDF Chat	The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories	2015	Peter LeFanu Lumsdaine Michael A. Warren	1
+	Banach-Mazur Computable Functions on Metric Spaces	2001	Peter Hertling	1
+	The Continuous Functionals	1999	Dag Normann	1
+ PDF Chat	Combining symbolic computation and theorem proving: Some problems of Ramanujan	1994	Edmund Clarke Xudong Zhao	1
+	On the interpretation of type theory in locally cartesian closed categories	1995	Martin Hofmann	1
+	Cartesian closed categories of domains	1989	Achim Jung	1
+ PDF Chat	Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo	2007	Denis Cousineau Gilles Dowek	1
+	A Survey of (∞, 1)-Categories	2009	Julia E. Bergner	1
+	Extensional concepts in intensional type theory	1995	Martin Hofmann	1