5 citations · 13 across the 5 of their papers we have counts for
5 papers
Embedding Pure Type Systems in the lambda-Pi-calculus modulo
Denis Cousineau, Gilles Dowek
The lambda-Pi-calculus allows to express proofs of minimal predicate logic. It can be extended, in a very simple way, by adding computation rules. This leads to the lambda-Pi-calcu…
Compositional pre-processing for automated reasoning in dependent type theory
Valentin Blot, Denis Cousineau, Enzo Crance +4
In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited…
Automated Deductive Verification for Ladder Programming
Denis Cousineau, David Mentré, Hiroaki Inoue
Ladder Logics is a programming language standardized in IEC 61131-3 and widely used for programming industrial Programmable Logic Controllers (PLC). A PLC program consists of input…
TLA+ Proofs
Denis Cousineau, Damien Doligez, Leslie Lamport +3
TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them wi…
On completeness of reducibility candidates as a semantics of strong normalization
Denis Cousineau
This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo à la Curry.…