17 citations · 73 across the 11 of their papers we have counts for
4 papers · 1 filter
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are ver…
A correspondence between rooted planar maps and normal planar lambda terms
Noam Zeilberger, Alain Giorgetti
A rooted planar map is a connected graph embedded in the 2-sphere, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be linear if ever…
Lazy AC-Pattern Matching for Rewriting
Walid Belkhir, Alain Giorgetti
We define a lazy pattern-matching mechanism modulo associativity and commutativity. The solutions of a pattern-matching problem are stored in a lazy list composed of a first substi…
Graph Based Reduction of Program Verification Conditions
Jean-François Couchot, Alain Giorgetti, Nicolas Stouls
Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler veri…