Publications

Bibliography

Selected publications

Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem (2025). Andrej Bauer. Journal of Logic and Analysis, vol. 17 (Article no. FDS3). DOI · arXiv · BibTeX

@article{bauer2025spreen,
  author    = {Andrej Bauer},
  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},
}

Incorporating a database of graphs into a proof assistant (2024). Andrej Bauer, Katja Berčič, Gauvain Devillez, Jure Taslak. Intelligent Computer Mathematics: 17th International Conference, CICM 2024, vol. 14960, pp. 146–162. DOI · BibTeX

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

MLFMF: Data sets for machine learning for mathematical formalization (2024). Andrej Bauer, Matej Petković, Ljupčo Todorovski. Advances in Neural Information Processing Systems 36 (NeurIPS 2023). DOI · arXiv · BibTeX

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

The passing of Marko Petkovšek (2023). Andrej Bauer, Sandi Klavžar. Annals of Combinatorics, vol. 27, no. 2, pp. 455–456. DOI · BibTeX

@article{bauer2023petkovsek,
  author    = {Andrej Bauer and Sandi Klavžar},
  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},
}

Finitary type theories with and without contexts (2023). Philipp Georg Haselwarter, Andrej Bauer. Journal of Automated Reasoning, vol. 67, no. 4 (Article no. 36). DOI · arXiv · BibTeX

@article{haselwarter2023finitary,
  author    = {Philipp Georg Haselwarter and Andrej Bauer},
  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},
}

An extensible equality checking algorithm for dependent type theories (2022). Andrej Bauer, Anja Petković Komel. Logical Methods in Computer Science, vol. 18, no. 1, pp. 17:1–17:42. DOI · arXiv · BibTeX

@article{bauer2022extensible,
  author    = {Andrej Bauer and Anja Petković Komel},
  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},
}

Instance reducibility and Weihrauch degrees (2022). Andrej Bauer. Logical Methods in Computer Science, vol. 18, no. 3, pp. 20:1–20:18. DOI · arXiv · BibTeX

@article{bauer2022instance,
  author    = {Andrej Bauer},
  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},
}

Runners in action (2020). Danel Ahman, Andrej Bauer. Programming Languages and Systems: 29th European Symposium on Programming, ESOP 2020, vol. 12075, pp. 29–55. DOI · arXiv · BibTeX

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

Equality checking for general type theories in Andromeda 2 (2020). Andrej Bauer, Philipp Georg Haselwarter, Anja Petković Komel. Mathematical Software — ICMS 2020, vol. 12097, pp. 253–259. DOI · BibTeX

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

Every metric space is separable in function realizability (2019). Andrej Bauer, Andrew W. Swan. Logical Methods in Computer Science, vol. 15, no. 2 (Article no. 14). DOI · arXiv · BibTeX

@article{bauer2019separable,
  author    = {Andrej Bauer and Andrew W. Swan},
  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},
}

Design and implementation of the Andromeda proof assistant (2018). Andrej Bauer, Gaëtan Gilbert, Philipp Georg Haselwarter, Matija Pretnar, Christopher A. Stone. 22nd International Conference on Types for Proofs and Programs (TYPES 2016), vol. 97, pp. 5:1–5:31. DOI · arXiv · BibTeX

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

A formalization of homotopy type theory in Coq (2017). Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, Bas Spitters. Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), pp. 164–172. DOI · BibTeX

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

Five stages of accepting constructive mathematics (2017). Andrej Bauer. Bulletin of the American Mathematical Society, vol. 54, no. 3, pp. 481–498. DOI · BibTeX

@article{bauer2017five,
  author    = {Andrej Bauer},
  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},
}

On fixed-point theorems in synthetic computability (2017). Andrej Bauer. Tbilisi Mathematical Journal, vol. 10, no. 3, pp. 167–181. DOI · BibTeX

@article{bauer2017fixedpoint,
  author    = {Andrej Bauer},
  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},
}

An injection from the Baire space to natural numbers (2015). Andrej Bauer. Mathematical Structures in Computer Science, vol. 25, no. 7, pp. 1484–1489. DOI · BibTeX

@article{bauer2015injection,
  author    = {Andrej Bauer},
  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},
}

Programming with algebraic effects and handlers (2015). Andrej Bauer, Matija Pretnar. Journal of Logical and Algebraic Methods in Programming, pp. 108–123. DOI · arXiv · BibTeX

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

Cartesian closed categories of separable Scott domains (2014). Andrej Bauer, Gordon Plotkin, Dana S. Scott. Theoretical Computer Science, vol. 546, pp. 17–29. DOI · BibTeX

@article{bauer2014cartesian,
  author    = {Andrej Bauer and Gordon Plotkin and Dana S. Scott},
  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},
}

An effect system for algebraic effects and handlers (2014). Andrej Bauer, Matija Pretnar. Logical Methods in Computer Science, vol. 10, no. 4, pp. 1–29 (Paper no. 9). DOI · arXiv · BibTeX

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

On the Bourbaki–Witt principle in toposes (2013). Andrej Bauer, Peter LeFanu Lumsdaine. Mathematical Proceedings of the Cambridge Philosophical Society, vol. 155, no. 1, pp. 87–99. DOI · arXiv · BibTeX

@article{bauer2013bourbaki,
  author    = {Andrej Bauer and Peter LeFanu Lumsdaine},
  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},
  doi       = {10.1017/S0305004113000108},
  eprint    = {1201.0340},
  eprinttype = {arXiv},
}

Intuitionistic mathematics and realizability in the physical world (2013). Andrej Bauer. In: A Computable Universe: Understanding and Exploring Nature as Computation, pp. 143–157. DOI · BibTeX

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

On monadic parametricity of second-order functionals (2013). Andrej Bauer, Martin Hofmann, Aleksandr Karbyshev. Foundations of Software Science and Computation Structures (FoSSaCS 2013), vol. 7794, pp. 225–240. DOI · BibTeX

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

A non-commutative Priestley duality (2013). Andrej Bauer, Karin Cvetko-Vah, Mai Gehrke, Samuel J. Van Gool, Ganna Kudryavtseva. Topology and its Applications, vol. 160, no. 12, pp. 1423–1438. BibTeX

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

Stone duality for skew Boolean algebras with intersections (2013). Andrej Bauer, Karin Cvetko-Vah. Houston Journal of Mathematics, vol. 39, no. 1, pp. 73–109. BibTeX

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

Homotopy Type Theory: Univalent Foundations of Mathematics (2013). The Univalent Foundations Program. . BibTeX

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

On the failure of fixed-point theorems for chain-complete lattices in the effective topos (2012). Andrej Bauer. Theoretical Computer Science, pp. 43–50. DOI · arXiv · BibTeX

@article{bauer2012fixedpoint,
  author    = {Andrej Bauer},
  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},
  doi       = {10.1016/j.tcs.2011.12.005},
  eprint    = {0911.0068},
  eprinttype = {arXiv},
}

Metric spaces in synthetic topology (2012). Andrej Bauer, Davorin Lešnik. Annals of Pure and Applied Logic, vol. 163, no. 2, pp. 87–100. DOI · BibTeX

@article{bauer2012metric,
  author    = {Andrej Bauer and Davorin Lešnik},
  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},
}

Canonical effective subalgebras of classical algebras as constructive metric completions (2010). Andrej Bauer, Jens Blanck. Journal of Universal Computer Science, pp. 2496–2522. DOI · BibTeX

@article{bauer2010canonical,
  author    = {Andrej Bauer and Jens Blanck},
  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},
}

A constructive theory of continuous domains suitable for implementation (2009). Andrej Bauer, Iztok Kavkler. Annals of Pure and Applied Logic, pp. 251–267. DOI · BibTeX

@article{bauer2009constructive,
  author    = {Andrej Bauer and Iztok Kavkler},
  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},
}

The Dedekind reals in abstract Stone duality (2009). Andrej Bauer, Paul Taylor. Mathematical Structures in Computer Science, vol. 19, no. 4, pp. 757–838. DOI · BibTeX

@article{bauer2009dedekind,
  author    = {Andrej Bauer and Paul Taylor},
  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},
}

RZ: a tool for bringing constructive and computable mathematics closer to programming practice (2009). Andrej Bauer, Christopher A. Stone. Journal of Logic and Computation, vol. 19, no. 1, pp. 17–43. DOI · BibTeX

@article{bauer2009rz,
  author    = {Andrej Bauer and Christopher A. Stone},
  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},
}

Sheaf toposes for realizability (2008). Steve Awodey, Andrej Bauer. Archive for Mathematical Logic, vol. 47, no. 5, pp. 465–478. DOI · BibTeX

@article{awodey2008sheaf,
  author    = {Steve Awodey and Andrej Bauer},
  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},
}

First steps in synthetic computability theory (2006). Andrej Bauer. Proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), vol. 155, pp. 5–31. DOI · BibTeX

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

Propositions as [Types] (2004). Steve Awodey, Andrej Bauer. Journal of Logic and Computation, vol. 14, no. 4, pp. 447–471. DOI · BibTeX

@article{awodey2004propositions,
  author    = {Steve Awodey and Andrej Bauer},
  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},
}

Equilogical spaces (2004). Andrej Bauer, Lars Birkedal, Dana S. Scott. Theoretical Computer Science, vol. 315, no. 1, pp. 35–59. DOI · BibTeX

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

Two constructive embedding-extension theorems with applications to continuity principles and to Banach–Mazur computability (2004). Andrej Bauer, Alex Simpson. Mathematical Logic Quarterly, vol. 50, no. 4/5, pp. 351–369. DOI · BibTeX

@article{bauer2004simpson,
  author    = {Andrej Bauer and Alex Simpson},
  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},
}

Comparing functional paradigms for exact real-number computation (2002). Andrej Bauer, Martín Hötzel Escardó, Alex Simpson. Automata, Languages and Programming: 29th International Colloquium (ICALP 2002), vol. 2380, pp. 488–500. DOI · BibTeX

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

A relationship between equilogical spaces and type two effectivity (2002). Andrej Bauer. Mathematical Logic Quarterly, vol. 48, no. Suppl. 1, pp. 1–15. DOI · BibTeX

@article{bauer2002relationship,
  author    = {Andrej Bauer},
  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},
}

Continuous functionals of dependent types and equilogical spaces (2000). Andrej Bauer, Lars Birkedal. Computer Science Logic: 14th International Workshop, CSL 2000, vol. 1862, pp. 202–216. DOI · BibTeX

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

The realizability approach to computable analysis and topology (2000). Andrej Bauer. PhD thesis, Carnegie Mellon University. PDF · BibTeX

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

Multibasic and mixed hypergeometric Gosper-type algorithms (1999). Andrej Bauer, Marko Petkovšek. Journal of Symbolic Computation, vol. 28, no. 4/5, pp. 711–736. DOI · BibTeX

@article{bauer1999multibasic,
  author    = {Andrej Bauer and Marko Petkovšek},
  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},
}

Analytica — An experiment in combining theorem proving and symbolic computation (1998). Andrej Bauer, Edmund Clarke, Xudong Zhao. Journal of Automated Reasoning, vol. 21, no. 3, pp. 295–325. DOI · BibTeX

@article{bauer1998analytica,
  author    = {Andrej Bauer and Edmund Clarke and Xudong Zhao},
  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},
}