| 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
Lecture Notes in Computer Science | 2022-08-30 | Paper |
Monotone recursive types and recursive data representations in Cedille
Mathematical Structures in Computer Science | 2022-05-17 | Paper |
| Efficient lambda encodings for Mendler-style coinductive types in Cedille | 2022-01-06 | Paper |
Efficient lambda encodings for Mendler-style coinductive types in Cedille
(available as arXiv preprint) | 2022-01-06 | Paper |
| Irrelevance, heterogeneous equality, and call-by-value dependent type systems | 2021-03-17 | Paper |
Irrelevance, heterogeneous equality, and call-by-value dependent type systems
(available as arXiv preprint) | 2021-03-17 | Paper |
| Equality, quasi-implicit products, and large eliminations | 2021-03-03 | Paper |
Equality, quasi-implicit products, and large eliminations
(available as arXiv preprint) | 2021-03-03 | Paper |
Efficient Mendler-style lambda-encodings in Cedille
(available as arXiv preprint) | 2018-10-04 | Paper |
From realizability to induction via dependent intersection
Annals of Pure and Applied Logic | 2018-06-05 | Paper |
The calculus of dependent lambda eliminations
Journal of Functional Programming | 2017-10-23 | Paper |
Efficiency of lambda-encodings in total type theory
Journal of Functional Programming | 2017-10-23 | Paper |
A lazy approach to adaptive exact real arithmetic using floating-point operations
ACM Communications in Computer Algebra | 2017-06-22 | Paper |
Dualized simple type theory
Logical Methods in Computer Science | 2017-04-11 | Paper |
The 2013 evaluation of SMT-COMP and SMT-LIB
Journal of Automated Reasoning | 2016-05-26 | Paper |
A language-based approach to functionally correct imperative programming
Proceedings of the tenth ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
Self types for dependently typed lambda encodings
Lecture Notes in Computer Science | 2014-07-24 | Paper |
SMT proof checking using a logical framework
Formal Methods in System Design | 2014-03-28 | Paper |
Imperative LF meta-programming
Electronic Notes in Theoretical Computer Science | 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
Logical Methods in Computer Science | 2013-04-09 | Paper |
versat: A Verified Modern SAT Solver
Lecture Notes in Computer Science | 2012-06-15 | Paper |
| Type Preservation as a Confluence Problem | 2012-04-24 | Paper |
Automated Deduction – CADE-19
Lecture Notes in Computer Science | 2010-04-20 | Paper |
Directly reflective meta-programming
Higher-Order and Symbolic Computation | 2010-03-05 | Paper |
Knuth-Bendix completion of theories of commuting group endomorphisms
Information Processing Letters | 2010-01-18 | Paper |
Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
Lecture Notes in Computer Science | 2008-09-25 | Paper |
Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
Formal Methods in System Design | 2007-11-28 | Paper |
Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
Journal of Automated Reasoning | 2007-01-30 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Term Rewriting and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
| scientific article; zbMATH DE number 2090315 (Why is no real title available?) | 2004-08-12 | Paper |
| scientific article; zbMATH DE number 2086596 (Why is no real title available?) | 2004-08-11 | Paper |
A trustworthy proof checker
Journal of Automated Reasoning | 2004-08-06 | Paper |
| scientific article; zbMATH DE number 1903374 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1903356 (Why is no real title available?) | 2003-05-01 | Paper |
| scientific article; zbMATH DE number 1614688 (Why is no real title available?) | 2001-07-05 | Paper |
