Autosubst 2: Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
(pdf)
Kathrin Stark, Steven Schäfer, Jonas Kaiser
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, 2019.
Binder Aware Recursion over Well-Scoped de Bruijn Syntax
(pdf)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
Certified Programs and Proofs - 7th International Conference, CPP 2018, Los Angeles, USA, January 8-9, 2018, 2018.
Autosubst 2: Towards Reasoning with Multi-Sorted de Bruijn Terms and Vector Substitutions
(pdf)
Jonas Kaiser, Steven Schäfer, Kathrin Stark
LFMTP, 2017.
Relating System F and λ2: A Case Study in Coq, Abella and Beluga
(pdf)
Jonas Kaiser, Brigitte Pientka, Gert Smolka
Proceedings of FSCD 2017, 2017.
Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas
(pdf)
Jonas Kaiser, Tobias Tebbi, Gert Smolka
Proceedings of CPP 2017, 2017.
Formal Verification of the Equivalence of System F and the Pure Type System L2
(pdf)
Jonas Kaiser
PhD Thesis, 2019.
Formal Costruction of a Set Theory in Coq
(pdf)
Jonas Kaiser
Master's Thesis, Programming Systems Lab, Saarland University, 2012.
Reconsidering Lucid - a modern approach
(pdf)
Jonas Kaiser
B.A. Dissertation, Churchill College, University of Cambridge, Bachelors Thesis, 2010.