| Publication | Date of Publication | Type |
|---|
| Simulating large eliminations in Cedille | 2024-08-01 | Paper |
| Impredicative encodings of inductive-inductive data in Cedille | 2024-02-28 | Paper |
| Quotients by idempotent functions in Cedille | 2022-08-30 | Paper |
| Monotone recursive types and recursive data representations in Cedille | 2022-05-17 | Paper |
| Efficient lambda encodings for Mendler-style coinductive types in Cedille | 2022-01-06 | Paper |
| Irrelevance, heterogeneous equality, and call-by-value dependent type systems | 2021-03-17 | Paper |
| Equality, quasi-implicit products, and large eliminations | 2021-03-03 | Paper |
| Efficient Mendler-style lambda-encodings in Cedille | 2018-10-04 | Paper |
| From realizability to induction via dependent intersection | 2018-06-05 | Paper |
| The calculus of dependent lambda eliminations | 2017-10-23 | Paper |
| Efficiency of lambda-encodings in total type theory | 2017-10-23 | Paper |
| A lazy approach to adaptive exact real arithmetic using floating-point operations | 2017-06-22 | Paper |
| Dualized simple type theory | 2017-04-11 | Paper |
| The 2013 evaluation of SMT-COMP and SMT-LIB | 2016-05-26 | Paper |
| A language-based approach to functionally correct imperative programming | 2015-01-06 | Paper |
| Self types for dependently typed lambda encodings | 2014-07-24 | Paper |
| SMT proof checking using a logical framework | 2014-03-28 | Paper |
| Imperative LF meta-programming | 2014-01-10 | Paper |
| Mining propositional simplification proofs for small validating clauses | 2013-09-26 | Paper |
| Validated proof-producing decision procedures | 2013-09-25 | Paper |
| Logical semantics for the rewriting calculus | 2013-09-25 | Paper |
| From Rogue to MicroRogue | 2013-09-20 | Paper |
| Producing proofs from an arithmetic decision procedure in elliptical LF | 2013-08-19 | Paper |
| A rewriting view of simple typing | 2013-04-09 | Paper |
| versat: A Verified Modern SAT Solver | 2012-06-15 | Paper |
| Type Preservation as a Confluence Problem | 2012-04-24 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Directly reflective meta-programming | 2010-03-05 | Paper |
| Knuth-Bendix completion of theories of commuting group endomorphisms | 2010-01-18 | Paper |
| Slothrop: Knuth-Bendix Completion with a Modern Termination Checker | 2008-09-25 | Paper |
| Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006) | 2007-11-28 | Paper |
| Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) | 2007-01-30 | Paper |
| Computer Aided Verification | 2006-01-10 | Paper |
| Term Rewriting and Applications | 2005-11-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4809074 | 2004-08-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4737130 | 2004-08-11 | Paper |
| A trustworthy proof checker | 2004-08-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804919 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4804899 | 2003-05-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2723410 | 2001-07-05 | Paper |
