| Publication | Date of Publication | Type |
|---|
Sharing proofs with predicative theories through universe-polymorphic elaboration
Logical Methods in Computer Science | 2024-11-12 | Paper |
| Translating proofs from an impredicative type system to a predicative one | 2024-09-25 | Paper |
| Encoding type universes without using matching modulo associativity and commutativity | 2024-05-27 | Paper |
| Some Axioms for Mathematics | 2023-06-23 | Paper |
A modular construction of type theories
Logical Methods in Computer Science | 2023-03-22 | Paper |
scientific article; zbMATH DE number 7559275 (Why is no real title available?)
(available as arXiv preprint) | 2022-07-18 | Paper |
Corrigendum to: ``Inductive-data-type systems
Theoretical Computer Science | 2020-04-01 | Paper |
Size-based termination of higher-order rewriting
Journal of Functional Programming | 2018-08-03 | Paper |
Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
Theoretical Computer Science | 2015-12-15 | Paper |
The computability path ordering
Logical Methods in Computer Science | 2015-10-29 | Paper |
| A point on fixpoints in posets | 2014-12-23 | Paper |
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
Mathematical Structures in Computer Science | 2011-10-21 | Paper |
On the confluence of lambda-calculus with conditional rewriting
Theoretical Computer Science | 2010-08-24 | Paper |
On the Relation between Sized-Types Based Termination and Semantic Labelling
Computer Science Logic | 2009-11-12 | Paper |
Rewriting Techniques and Applications
Lecture Notes in Computer Science | 2009-04-30 | Paper |
Computability Closure: Ten Years Later
Rewriting, Computation and Proof | 2009-03-06 | Paper |
Building Decision Procedures in the Calculus of Inductive Constructions
Computer Science Logic | 2009-03-05 | Paper |
The Computability Path Ordering: The End of a Quest
Computer Science Logic | 2008-11-20 | Paper |
Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Higher-Order Termination: From Kruskal to Computability
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
HORPO with Computability Closure: A Reconstruction
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-15 | Paper |
On the Implementation of Construction Functions for Non-free Concrete Data Types
Programming Languages and Systems | 2007-09-04 | Paper |
Foundations of Software Science and Computation Structures
Lecture Notes in Computer Science | 2007-05-02 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2006-11-01 | Paper |
| scientific article; zbMATH DE number 2182487 (Why is no real title available?) | 2005-06-23 | Paper |
Definitions by rewriting in the Calculus of Constructions
Mathematical Structures in Computer Science | 2005-03-14 | Paper |
| scientific article; zbMATH DE number 2061701 (Why is no real title available?) | 2004-03-22 | Paper |
| scientific article; zbMATH DE number 2043543 (Why is no real title available?) | 2004-02-16 | Paper |
Inductive-data-type systems
Theoretical Computer Science | 2002-03-03 | Paper |
| scientific article; zbMATH DE number 1615229 (Why is no real title available?) | 2001-07-08 | Paper |
| scientific article; zbMATH DE number 1405632 (Why is no real title available?) | 2000-09-13 | Paper |
