% Selected publications of Andrej Bauer
%
% This is the primary source for the publications list on andrej.com.
% The file _data/publications.yml (used to render the HTML page) is generated
% from this file — do not edit it directly.
% After making changes, regenerate it with:
%
%   python3 bib2data.py
%
% Conventions:
%   Use UTF-8 characters directly (š, č, ž, ü, é, …) — no LaTeX encoding.
%   Extra fields:
%   doi        = {10.xxxx/yyyy}           DOI, used aggressively when available
%   eprint     = {YYMM.NNNNN}            arXiv identifier
%   eprinttype = {arXiv}                  always paired with eprint
%   pdf        = {filename.pdf}           local PDF in /assets/papers/
%
% One entry per paper. When a paper has both a conference version and a
% journal version, keep the journal version and add the arXiv eprint if
% available. Conference-only papers are kept as @inproceedings.

% ---------------------------------------------------------------------------
% 2025
% ---------------------------------------------------------------------------

@article{bauer2025spreen,
  author     = {Bauer, Andrej},
  title      = {Spreen spaces and the synthetic {Kreisel-Lacombe-Shoenfield-Tseitin} theorem},
  journal    = {Journal of Logic and Analysis},
  year       = {2025},
  volume     = {17},
  note       = {Article no.\ FDS3},
  doi        = {10.4115/jla.2025.17.FDS3},
  eprint     = {2307.07830},
  eprinttype = {arXiv},
}

% ---------------------------------------------------------------------------
% 2024
% ---------------------------------------------------------------------------

@inproceedings{bauer2024cicm,
  author    = {Bauer, Andrej and Berčič, Katja and Devillez, Gauvain and Taslak, Jure},
  title     = {Incorporating a database of graphs into a proof assistant},
  booktitle = {Intelligent Computer Mathematics: 17th International Conference, {CICM}~2024},
  publisher = {Springer},
  year      = {2024},
  editor    = {Kohlhase, Andrea and Kovács, Laura},
  series    = {Lecture Notes in Artificial Intelligence},
  volume    = {14960},
  pages     = {146--162},
  address   = {Cham},
  doi       = {10.1007/978-3-031-66997-2_9},
}

@inproceedings{bauer2024mlfmf,
  author     = {Bauer, Andrej and Petković, Matej and Todorovski, Ljupčo},
  title      = {{MLFMF}: Data sets for machine learning for mathematical formalization},
  booktitle  = {Advances in Neural Information Processing Systems 36 ({NeurIPS}~2023)},
  publisher  = {Curran Associates},
  year       = {2024},
  doi        = {10.5555/3666122.3668329},
  eprint     = {2310.16005},
  eprinttype = {arXiv},
}

% ---------------------------------------------------------------------------
% 2023
% ---------------------------------------------------------------------------

@article{haselwarter2023finitary,
  author     = {Haselwarter, Philipp Georg and Bauer, Andrej},
  title      = {Finitary type theories with and without contexts},
  journal    = {Journal of Automated Reasoning},
  year       = {2023},
  volume     = {67},
  number     = {4},
  note       = {Article no. 36},
  doi        = {10.1007/s10817-023-09678-y},
  eprint     = {2112.00539},
  eprinttype = {arXiv},
}

@article{bauer2023petkovsek,
  author  = {Bauer, Andrej and Klavžar, Sandi},
  title   = {The passing of {Marko Petkovšek}},
  journal = {Annals of Combinatorics},
  year    = {2023},
  volume  = {27},
  number  = {2},
  pages   = {455--456},
  doi     = {10.1007/s00026-023-00653-3},
}

% ---------------------------------------------------------------------------
% 2022
% ---------------------------------------------------------------------------

@article{bauer2022extensible,
  author     = {Bauer, Andrej and Petković Komel, Anja},
  title      = {An extensible equality checking algorithm for dependent type theories},
  journal    = {Logical Methods in Computer Science},
  year       = {2022},
  volume     = {18},
  number     = {1},
  pages      = {17:1--17:42},
  doi        = {10.46298/lmcs-18(1:17)2022},
  eprint     = {2103.07397},
  eprinttype = {arXiv},
}

@article{bauer2022instance,
  author     = {Bauer, Andrej},
  title      = {Instance reducibility and {Weihrauch} degrees},
  journal    = {Logical Methods in Computer Science},
  year       = {2022},
  volume     = {18},
  number     = {3},
  pages      = {20:1--20:18},
  doi        = {10.46298/lmcs-18(3:20)2022},
  eprint     = {2106.01734},
  eprinttype = {arXiv},
}

% ---------------------------------------------------------------------------
% 2020
% ---------------------------------------------------------------------------

@inproceedings{ahman2020runners,
  author     = {Ahman, Danel and Bauer, Andrej},
  title      = {Runners in action},
  booktitle  = {Programming Languages and Systems: 29th European Symposium on Programming, {ESOP}~2020},
  publisher  = {Springer},
  year       = {2020},
  editor     = {Müller, Peter},
  series     = {Lecture Notes in Computer Science},
  volume     = {12075},
  pages      = {29--55},
  address    = {Cham},
  doi        = {10.1007/978-3-030-44914-8_2},
  eprint     = {1910.11629},
  eprinttype = {arXiv},
}

@inproceedings{bauer2020andromeda,
  author    = {Bauer, Andrej and Haselwarter, Philipp Georg and Petković Komel, Anja},
  title     = {Equality checking for general type theories in {Andromeda~2}},
  booktitle = {Mathematical Software --- {ICMS}~2020},
  publisher = {Springer},
  year      = {2020},
  editor    = {Bigatti, Anna Maria and others},
  series    = {Lecture Notes in Computer Science},
  volume    = {12097},
  pages     = {253--259},
  address   = {Cham},
  doi       = {10.1007/978-3-030-52200-1_25},
}

% ---------------------------------------------------------------------------
% 2019
% ---------------------------------------------------------------------------

@article{bauer2019separable,
  author     = {Bauer, Andrej and Swan, Andrew W.},
  title      = {Every metric space is separable in function realizability},
  journal    = {Logical Methods in Computer Science},
  year       = {2019},
  volume     = {15},
  number     = {2},
  note       = {Article no. 14},
  doi        = {10.23638/LMCS-15(2:14)2019},
  eprint     = {1804.00427},
  eprinttype = {arXiv},
}

% ---------------------------------------------------------------------------
% 2018
% ---------------------------------------------------------------------------

@inproceedings{bauer2018andromeda,
  author     = {Bauer, Andrej and Gilbert, Gaëtan and Haselwarter, Philipp Georg and Pretnar, Matija and Stone, Christopher A.},
  title      = {Design and implementation of the {Andromeda} proof assistant},
  booktitle  = {22nd International Conference on Types for Proofs and Programs ({TYPES}~2016)},
  publisher  = {Schloss Dagstuhl, Leibniz-Zentrum für Informatik},
  year       = {2018},
  editor     = {Ghilezan, Silvia and Geuvers, Herman and Ivetić, Jelena},
  series     = {Leibniz International Proceedings in Informatics},
  volume     = {97},
  pages      = {5:1--5:31},
  address    = {Dagstuhl},
  doi        = {10.4230/LIPIcs.TYPES.2016.5},
  eprint     = {1802.06217},
  eprinttype = {arXiv},
}

% ---------------------------------------------------------------------------
% 2017
% ---------------------------------------------------------------------------

@article{bauer2017five,
  author  = {Bauer, Andrej},
  title   = {Five stages of accepting constructive mathematics},
  journal = {Bulletin of the American Mathematical Society},
  year    = {2017},
  volume  = {54},
  number  = {3},
  pages   = {481--498},
  doi     = {10.1090/bull/1556},
}

@article{bauer2017fixedpoint,
  author  = {Bauer, Andrej},
  title   = {On fixed-point theorems in synthetic computability},
  journal = {Tbilisi Mathematical Journal},
  year    = {2017},
  volume  = {10},
  number  = {3},
  pages   = {167--181},
  doi     = {10.1515/tmj-2017-0107},
}

@inproceedings{bauer2017coq,
  author    = {Bauer, Andrej and Gross, Jason and Lumsdaine, Peter LeFanu and Shulman, Michael and Sozeau, Matthieu and Spitters, Bas},
  title     = {A formalization of homotopy type theory in {Coq}},
  booktitle = {Proceedings of the 6th {ACM} {SIGPLAN} Conference on Certified Programs and Proofs ({CPP}~2017)},
  publisher = {ACM},
  year      = {2017},
  editor    = {Bertot, Yves and Vafeiadis, Viktor},
  pages     = {164--172},
  address   = {New York},
  doi       = {10.1145/3018610.3018615}
}

% ---------------------------------------------------------------------------
% 2015
% ---------------------------------------------------------------------------

@article{bauer2015programming,
  author     = {Bauer, Andrej and Pretnar, Matija},
  title      = {Programming with algebraic effects and handlers},
  journal    = {Journal of Logical and Algebraic Methods in Programming},
  year       = {2015},
  pages      = {108--123},
  eprint     = {1203.1539},
  eprinttype = {arXiv},
  doi        = {10.1016/j.jlamp.2014.02.001}
}

@article{bauer2015injection,
  author  = {Bauer, Andrej},
  title   = {An injection from the {Baire} space to natural numbers},
  journal = {Mathematical Structures in Computer Science},
  year    = {2015},
  volume  = {25},
  number  = {7},
  pages   = {1484--1489},
  doi     = {10.1017/S0960129513000406}
}

% ---------------------------------------------------------------------------
% 2014
% ---------------------------------------------------------------------------

@article{bauer2014effectsystem,
  author     = {Bauer, Andrej and Pretnar, Matija},
  title      = {An effect system for algebraic effects and handlers},
  journal    = {Logical Methods in Computer Science},
  year       = {2014},
  volume     = {10},
  number     = {4},
  note       = {Paper no. 9},
  pages      = {1--29},
  eprint     = {1306.6316},
  eprinttype = {arXiv},
  doi        = {10.2168/LMCS-10(4:9)2014}
}

@article{bauer2014cartesian,
  author  = {Bauer, Andrej and Plotkin, Gordon and Scott, Dana S.},
  title   = {Cartesian closed categories of separable {Scott} domains},
  journal = {Theoretical Computer Science},
  year    = {2014},
  volume  = {546},
  pages   = {17--29},
  doi     = {10.1016/j.tcs.2014.02.042}
}

% ---------------------------------------------------------------------------
% 2013
% ---------------------------------------------------------------------------

@book{hott2013book,
  author    = {{The Univalent Foundations Program}},
  title     = {Homotopy Type Theory: Univalent Foundations of Mathematics},
  publisher = {Institute for Advanced Study},
  year      = {2013},
  address   = {Princeton},
  url       = {https://homotopytypetheory.org/book},
}

@incollection{bauer2013intuitionistic,
  author    = {Bauer, Andrej},
  title     = {Intuitionistic mathematics and realizability in the physical world},
  booktitle = {A Computable Universe: Understanding and Exploring Nature as Computation},
  publisher = {World Scientific},
  year      = {2013},
  editor    = {Zenil, Hector},
  pages     = {143--157},
  address   = {Singapore},
  doi       = {10.1142/9789814374309_0008},
}

@inproceedings{bauer2013monadic,
  author    = {Bauer, Andrej and Hofmann, Martin and Karbyshev, Aleksandr},
  title     = {On monadic parametricity of second-order functionals},
  booktitle = {Foundations of Software Science and Computation Structures ({FoSSaCS}~2013)},
  publisher = {Springer},
  year      = {2013},
  editor    = {Pfenning, Frank},
  series    = {Lecture Notes in Computer Science},
  volume    = {7794},
  pages     = {225--240},
  address   = {Berlin},
  doi       = {10.1007/978-3-642-37075-5_15}
}

@article{bauer2013stone,
  author  = {Bauer, Andrej and Cvetko-Vah, Karin},
  title   = {Stone duality for skew {Boolean} algebras with intersections},
  journal = {Houston Journal of Mathematics},
  year    = {2013},
  volume  = {39},
  number  = {1},
  pages   = {73--109},
}

@article{bauer2013bourbaki,
  author     = {Bauer, Andrej and Lumsdaine, Peter LeFanu},
  title      = {On the {Bourbaki--Witt} principle in toposes},
  journal    = {Mathematical Proceedings of the Cambridge Philosophical Society},
  year       = {2013},
  volume     = {155},
  number     = {1},
  pages      = {87--99},
  eprint     = {1201.0340},
  eprinttype = {arXiv},
  doi        = {10.1017/S0305004113000108}
}

@article{bauer2013priestley,
  author  = {Bauer, Andrej and Cvetko-Vah, Karin and Gehrke, Mai and {Van Gool}, Samuel J. and Kudryavtseva, Ganna},
  title   = {A non-commutative {Priestley} duality},
  journal = {Topology and its Applications},
  year    = {2013},
  volume  = {160},
  number  = {12},
  pages   = {1423--1438},
}

% ---------------------------------------------------------------------------
% 2012
% ---------------------------------------------------------------------------

@article{bauer2012fixedpoint,
  author     = {Bauer, Andrej},
  title      = {On the failure of fixed-point theorems for chain-complete lattices in the effective topos},
  journal    = {Theoretical Computer Science},
  year       = {2012},
  pages      = {43--50},
  eprint     = {0911.0068},
  eprinttype = {arXiv},
  doi        = {10.1016/j.tcs.2011.12.005}
}

@article{bauer2012metric,
  author  = {Bauer, Andrej and Lešnik, Davorin},
  title   = {Metric spaces in synthetic topology},
  journal = {Annals of Pure and Applied Logic},
  year    = {2012},
  volume  = {163},
  number  = {2},
  pages   = {87--100},
  doi     = {10.1016/j.apal.2011.06.017}
}

% ---------------------------------------------------------------------------
% 2010
% ---------------------------------------------------------------------------

@article{bauer2010canonical,
  author  = {Bauer, Andrej and Blanck, Jens},
  title   = {Canonical effective subalgebras of classical algebras as constructive metric completions},
  journal = {Journal of Universal Computer Science},
  year    = {2010},
  pages   = {2496--2522},
  doi     = {10.3217/jucs-016-18-2496}
}

% ---------------------------------------------------------------------------
% 2009
% ---------------------------------------------------------------------------

@article{bauer2009rz,
  author  = {Bauer, Andrej and Stone, Christopher A.},
  title   = {{RZ}: a tool for bringing constructive and computable mathematics closer to programming practice},
  journal = {Journal of Logic and Computation},
  year    = {2009},
  volume  = {19},
  number  = {1},
  pages   = {17--43},
  doi     = {10.1007/978-3-540-73001-9_4}
}

@article{bauer2009dedekind,
  author  = {Bauer, Andrej and Taylor, Paul},
  title   = {The {Dedekind} reals in abstract {Stone} duality},
  journal = {Mathematical Structures in Computer Science},
  year    = {2009},
  volume  = {19},
  number  = {4},
  pages   = {757--838},
  doi     = {10.1017/S0960129509007695}
}

@article{bauer2009constructive,
  author  = {Bauer, Andrej and Kavkler, Iztok},
  title   = {A constructive theory of continuous domains suitable for implementation},
  journal = {Annals of Pure and Applied Logic},
  year    = {2009},
  pages   = {251--267},
  doi     = {10.1016/j.apal.2008.09.025}
}

% ---------------------------------------------------------------------------
% 2008
% ---------------------------------------------------------------------------

@article{awodey2008sheaf,
  author  = {Awodey, Steve and Bauer, Andrej},
  title   = {Sheaf toposes for realizability},
  journal = {Archive for Mathematical Logic},
  year    = {2008},
  volume  = {47},
  number  = {5},
  pages   = {465--478},
  doi     = {10.1007/s00153-008-0090-6}
}

% ---------------------------------------------------------------------------
% 2006
% ---------------------------------------------------------------------------

@inproceedings{bauer2006firststeps,
  author    = {Bauer, Andrej},
  title     = {First steps in synthetic computability theory},
  booktitle = {Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics ({MFPS}~{XXI})},
  publisher = {Elsevier},
  year      = {2006},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {155},
  pages     = {5--31},
  address   = {Amsterdam},
  doi       = {10.1016/j.entcs.2005.11.049}
}

% ---------------------------------------------------------------------------
% 2004
% ---------------------------------------------------------------------------

@article{awodey2004propositions,
  author  = {Awodey, Steve and Bauer, Andrej},
  title   = {Propositions as {[Types]}},
  journal = {Journal of Logic and Computation},
  year    = {2004},
  volume  = {14},
  number  = {4},
  pages   = {447--471},
  doi     = {10.1093/logcom/14.4.447}
}

@article{bauer2004simpson,
  author  = {Bauer, Andrej and Simpson, Alex},
  title   = {Two constructive embedding-extension theorems with applications to continuity principles and to {Banach--Mazur} computability},
  journal = {Mathematical Logic Quarterly},
  year    = {2004},
  volume  = {50},
  number  = {4/5},
  pages   = {351--369},
  doi     = {10.1002/malq.200310104}
}

@article{bauer2004equilogical,
  author  = {Bauer, Andrej and Birkedal, Lars and Scott, Dana S.},
  title   = {Equilogical spaces},
  journal = {Theoretical Computer Science},
  year    = {2004},
  volume  = {315},
  number  = {1},
  pages   = {35--59},
  doi     = {10.1016/S0304-3975(03)00616-9},
}

% ---------------------------------------------------------------------------
% 2002
% ---------------------------------------------------------------------------

@inproceedings{bauer2002comparing,
  author    = {Bauer, Andrej and {Hötzel Escardó}, Martín and Simpson, Alex},
  title     = {Comparing functional paradigms for exact real-number computation},
  booktitle = {Automata, Languages and Programming: 29th International Colloquium ({ICALP}~2002)},
  publisher = {Springer},
  year      = {2002},
  editor    = {Widmayer, Peter and others},
  series    = {Lecture Notes in Computer Science},
  volume    = {2380},
  pages     = {488--500},
  address   = {Berlin},
  doi       = {10.1007/3-540-45465-9_42}
}

@article{bauer2002relationship,
  author  = {Bauer, Andrej},
  title   = {A relationship between equilogical spaces and type two effectivity},
  journal = {Mathematical Logic Quarterly},
  year    = {2002},
  volume  = {48},
  number  = {Suppl. 1},
  pages   = {1--15},
  doi     = {10.1002/1521-3870(200210)48:1+%3C1::AID-MALQ11111%3E3.0.CO;2-7}
}

% ---------------------------------------------------------------------------
% 2000
% ---------------------------------------------------------------------------

@inproceedings{bauer2000csl,
  author    = {Bauer, Andrej and Birkedal, Lars},
  title     = {Continuous functionals of dependent types and equilogical spaces},
  booktitle = {Computer Science Logic: 14th International Workshop, {CSL}~2000},
  publisher = {Springer},
  year      = {2000},
  editor    = {Clote, Peter G. and Schwichtenberg, Helmut},
  series    = {Lecture Notes in Computer Science},
  volume    = {1862},
  pages     = {202--216},
  address   = {Berlin},
  doi       = {10.1007/3-540-44622-2_13}
}

@phdthesis{bauer2000phd,
  author  = {Bauer, Andrej},
  title   = {The realizability approach to computable analysis and topology},
  school  = {Carnegie Mellon University},
  year    = {2000},
  address = {Pittsburgh},
  pdf     = {thesis.pdf}
}

% ---------------------------------------------------------------------------
% 1999
% ---------------------------------------------------------------------------

@article{bauer1999multibasic,
  author  = {Bauer, Andrej and Petkovšek, Marko},
  title   = {Multibasic and mixed hypergeometric {Gosper}-type algorithms},
  journal = {Journal of Symbolic Computation},
  year    = {1999},
  volume  = {28},
  number  = {4/5},
  pages   = {711--736},
  doi     = {10.1006/jsco.1999.0321}
}

% ---------------------------------------------------------------------------
% 1998
% ---------------------------------------------------------------------------

@article{bauer1998analytica,
  author  = {Bauer, Andrej and Clarke, Edmund and Zhao, Xudong},
  title   = {Analytica --- {An} experiment in combining theorem proving and symbolic computation},
  journal = {Journal of Automated Reasoning},
  year    = {1998},
  volume  = {21},
  number  = {3},
  pages   = {295--325},
  doi     = {10.1023/A:1006079212546}
}