Enrico Tassi

Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming, 2024

2023

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.

[BibT_eX]

[DOI]

Benjamin Grégoire

Jean-Christophe Léchenet

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

Reliably Reproducing Machine-Checked Proofs with the Coq Platform.

[BibT_eX]

[DOI]

Karl Palmskog

Théo Zimmermann

CoRR, 2022

2020

Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description).

[BibT_eX]

[DOI]

Cyril Cohen

Kazuhiko Sakaguchi

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

2019

Implementing type theory in higher order constraint logic programming.

[BibT_eX]

[DOI]

Ferruccio Guidi

Math. Struct. Comput. Sci., 2019

Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

2018

Coqoon - An IDE for interactive proof development in Coq.

[BibT_eX]

[DOI]

Alexander John Faithfull

Jesper Bengtson

Carst Tankink

Int. J. Softw. Tools Technol. Transf., 2018

2016

Implementing HOL in an Higher Order Logic Programming Language.

[BibT_eX]

[DOI]

Cvetan Dunchev

Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2016

2015

ELPI: Fast, Embeddable, λProlog Interpreter.

[BibT_eX]

[DOI]

Cvetan Dunchev

Ferruccio Guidi

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Asynchronous Processing of Coq Documents: From the Kernel up to the User Interface.

[BibT_eX]

[DOI]

Bruno Barras

Carst Tankink

Lourdes Del Carmen González-Huesca

Proceedings of the Interactive Theorem Proving - 6th International Conference, 2015

2014

A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3).

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems.

[BibT_eX]

[DOI]

Bruno Barras

Proceedings of the Intelligent Computer Mathematics, 2013

Canonical Structures for the Working Coq User.

[BibT_eX]

[DOI]

Assia Mahboubi

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

A Machine-Checked Proof of the Odd Order Theorem.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

A Language of Patterns for Subterm Selection.

[BibT_eX]

[DOI]

Georges Gonthier

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Formalising Overlap Algebras in Matita.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2011

The Matita Interactive Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Regular Expressions, au point

[BibT_eX]

[DOI]

CoRR, 2010

Smart Matching.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Nonuniform Coercions via Unification Hints

[BibT_eX]

[DOI]

Proceedings of the Proceedings Types for Proofs and Programs, Revised Selected Papers, 2009

Superposition as a logical glue

[BibT_eX]

[DOI]

Proceedings of the Proceedings Types for Proofs and Programs, Revised Selected Papers, 2009

Hints in Unification.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Natural Deduction Environment for Matita.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

2008

Interactive theorem provers: issues faced as a user and tackled as a developer.

[BibT_eX]

[DOI]

PhD thesis, 2008

A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2008

An Interactive Driver for Goal-directed Proof Strategies.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

2007

User Interaction with the Matita Proof Assistant.

[BibT_eX]

[DOI]

J. Autom. Reason., 2007

Working with Mathematical Structures in Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Conference, 2007

A Modular Formalisation of Finite Group Theory.

[BibT_eX]

[DOI]

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case.

[BibT_eX]

[DOI]

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

Tinycals: Step by Step Tacticals.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

Crafting a Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2006

2004

A Content Based Mathematical Search Engine: Whelp.

[BibT_eX]

[DOI]

Ferruccio Guidi