Publications

Papers

• Andrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone. Design and implementation of the Andromeda proof assistant. 22nd International Conference on Types for Proofs and Programs (TYPES 2016), May 2016, Novi Sad, Serbia.

• Andrej Bauer, Anja Petković Komel. An extensible equality checking algorithm for dependent type theories. Logical Methods in Computer Science, January 19, 2022, Volume 18, Issue 1.

• Andrej Bauer, Philipp G. Haselwarter, Anja Petković Komel. Equality Checking for General Type Theories in Andromeda 2 Mathematical Software – ICMS 2020. Lecture Notes in Computer Science, volume 12097, pages 253–259, Springer.

• Philipp G. Haselwarter, Andrej Bauer. Finitary Type Theories With and Without Contexts. Journal of Automated Reasoning, Volume 67, article number 36, October 2023.

Talks

• Andrej Bauer. Derivations as computations. Invited keynote talk. 24th ACM SIGPLAN International Conference on Functional Programming – ICFP 2019, August 2019, Berlin, Germany. (slides)

• Philipp G. Haselwarter, Andrej Bauer. Type theories without contexts. 27th International Conference on Types for Proofs and Programs, 14–18 June 2021, online. (slides)

• Anja Petković Komel. Equality Checking for Finitary Type Theories HoTTEST Conference 2020, June 18, 2020 (slides)