nLab Andrej Bauer

• home page

• blog

Selected writings

On propositional truncation in dependent type theory:

• Steve Awodey, Andrej Bauer, Propositions as $[$Types$]$, Journal of Logic and Computation, 14 (2004) 447-471 [doi:10.1093/logcom/14.4.447, pdf]

On the Dedekind real numbers via abstract Stone duality:

• Andrej Bauer, Paul Taylor, The Dedekind reals in abstract Stone duality, Mathematical Structures in Computer Science 19 4 (2009) 757-838 [doi:10.1017/S0960129509007695]

• Andrej Bauer, Efficient Computation with Dedekind Reals, talk at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008 (2008) [web, slides: pdf, extended abstract: pdf]

On the HoTT book real numbers:

• Andrej Bauer, The real numbers in homotopy type theory, talk at Computability and Complexity in Analysis, Faro (2016) [pdf, pdf]

On dependent type theory:

• Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine, A general definition of dependent type theories [arXiv:2009.05539]

On categorical logic:

• Steve Awodey, Andrej Bauer: Introduction to categorical logic, lecture notes for a course at Carnegie Mellon University (January-April 2024) [webpage, 0:pdf, 1:pdf, 2:pdf, 3:pdf, 4:pdf]

category: people