Author of the publication

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.

, , , and . FLOPS, volume 3945 of Lecture Notes in Computer Science, page 114-129. Springer, (2006)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Expression Reduction Systems with Patterns., and . RTA, volume 2706 of Lecture Notes in Computer Science, page 107-122. Springer, (2003)Certifying a Termination Criterion Based on Graphs, without Graphs., , and . TPHOLs, volume 5170 of Lecture Notes in Computer Science, page 183-198. Springer, (2008)Automated Certified Proofs with CiME3., , , , and . RTA, volume 10 of LIPIcs, page 21-30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2011)Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant., , , and . FLOPS, volume 3945 of Lecture Notes in Computer Science, page 114-129. Springer, (2006)A Weak Calculus with Explicit Operators for Pattern Matching and Substitution.. RTA, volume 2378 of Lecture Notes in Computer Science, page 174-191. Springer, (2002)A3PAT, an approach for certified automated termination proofs., , , , , and . PEPM, page 63-72. ACM, (2010)Certification of Automated Termination Proofs., , , , and . FroCoS, volume 4720 of Lecture Notes in Computer Science, page 148-162. Springer, (2007)