research
∙
08/29/2023
Sharing proofs with predicative theories through universe polymorphic elaboration
As the development of formal proofs is a time-consuming task, it is impo...
share
research
∙
11/10/2022
Translating proofs from an impredicative type system to a predicative one
As the development of formal proofs is a time-consuming task, it is impo...
research
∙
10/31/2021
Some axioms for mathematics
The lambda-Pi-calculus modulo theory is a logical framework in which man...
research
∙
10/26/2021
Encoding of Predicate Subtyping with Proof Irrelevance in the λΠ-Calculus Modulo Theory
The λΠ-calculus modulo theory is a logical framework in which various lo...
research
∙
10/30/2020
The New Rewriting Engine of Dedukti
Dedukti is a type-checker for the λΠ-calculus modulo rewriting, an exten...
research
∙
10/30/2020
Type safety of rewrite rules in dependent types
The expressiveness of dependent type theory can be extended by identifyi...
research
∙
08/26/2019
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract)
Proof assistants often call automated theorem provers to prove subgoals....
research
∙
06/27/2019
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Dependency pairs are a key concept at the core of modern automated termi...
research
∙
12/05/2018
Termination of λΠ modulo rewriting using the size-change principle (work in progress)
The Size-Change Termination principle was first introduced to study the ...
research
∙
07/03/2018
Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
This volume contains a selection of papers presented at LFMTP 2018, the ...
research
∙
04/24/2018
Higher-order dependency pairs
Arts and Giesl proved that the termination of a first-order rewrite syst...
research
∙
02/19/2018