Publications

To contribute to the web site, please open an issue, create a pull request or send a mail to the science communication coordinators.

2023

• A modular construction of type theories, Frédéric Blanqui, Gilles Dowek, Emilie Grienenberger, Gabriel Hondet and François Thiré, to appear in Logical Methods in Computer Science (LMCS)

• Translating proofs from an impredicative type system to a predicative one, T. Felicissimo, F. Blanqui and A. Kumar Barnawal, CSL’23

2022

• Theorem Proving for Maude Specifications Using Lean, Rubén Rubio and Adrián Riesco, ICFEM’22

• An Implementation of Set Theory with Pointed Graphs in Dedukti, Valentin Blot, Gilles Dowek and Thomas Traversié, LFMTP’22

• Evolution of Automated Deduction and Dynamic Constructions in Geometry, Pedro Quaresma, Mathematics Education in the Age of Artificial Intelligence, 2022

• Four Geometry Problems to Introduce Automated Deduction in Secondary Schools, Pedro Quaresma, Vanda Santos, ThEdu’21

• Lemmaless Induction in Trace Logic, Ahmed Bhayat, Pamina Georgiou, Clemens Eisenhofer, Laura Kovács, Giles Reger, CICM’22

• The Logic Languages of the TPTP World, Geoff Sutcliffe, Logic Journal of the IGPL, 2022

• Learning Higher-Order Logic Programs From Failures, Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk, IJCAI’22

• Adequate and Computational Encodings in the Logical Framework Dedukti, Thiago Felicissimo, FSCD’22

• Encoding Type Universes Without Using Matching Modulo Associativity and Commutativity, Frédéric Blanqui, FSCD’22

• Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting, Michael Färber, CPP’22

• What Can Formal Systems Do For Mathematics? A Discussion Through The Lens Of Proof Assistants: Some Recent Advances, Angeliki Koutsoukou-Argyraki Q&A with Jeremy Avigad, Jasmin Blanchette, Frédéric Blanqui, Kevin Buzzard, Johan Commelin, Manuel Eberl, Timothy Gowers, Peter Koepke, Assia Mahboubi, Ursula Martin, Lawrence C. Paulson, Special Issue for the 60th Anniversary of the DVMLG (German Association for Mathematical Logic and for Basic Research in the Exact Sciences), Benedikt Löwe, Deniz Sarikaya (eds.), College Publications, 2022

• Vers une traduction de K en Dedukti (Towards a translation of K in Dedukti), Amélie Ledein, Valentin Blot, Catherine Dubois, JFLA’22

• Bécassine à la chasse au Coq, Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial, JFLA’22

Reports

• WG3 kick-off meeting, Valencia, 10-11 February 2022 Slides&Videos Report