Claudio Sacerdoti Coen

According to our database, Claudio Sacerdoti Coen authored at least 74 papers between 2001 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2025

Thinking Machines: Mathematical Reasoning in the Age of LLMs.

Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen

CoRR, August, 2025

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines.

Beniamino Accattoli, Dan Ghica, Giulio Guerrieri, Cláudio Belo Lourenço, Claudio Sacerdoti Coen

CoRR, July, 2025

Positive Sharing and Abstract Machines.

Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu

CoRR, June, 2025

Indexing and Retrieval in a Heterogeneous Formal Library.

Claudio Sacerdoti Coen, Abdelghani Alidra

Proceedings of the Intelligent Computer Mathematics - 18th International Conference, 2025

The Cost of Skeletal Call-By-Need, Smoothly.

Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, Claudio Sacerdoti Coen

Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction, 2025

2024

sesame.

Claudio Sacerdoti Coen

Dataset, November, 2024

Reversible debugging of concurrent Erlang programs: Supporting imperative primitives.

Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, Giovanni Fabbretti

J. Log. Algebraic Methods Program., 2024

IMELL Cut Elimination with Linear Overhead.

Beniamino Accattoli, Claudio Sacerdoti Coen

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

2023

Causal Reversibility Implies Time Reversibility.

Marco Bernardo, Ivan Lanese, Andrea Marin, Claudio Antares Mezzina, Sabina Rossi, Claudio Sacerdoti Coen

Proceedings of the Quantitative Evaluation of Systems - 20th International Conference, 2023

Formalizing Functions as Processes.

Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Properties of a Computational Lambda Calculus for Higher-Order Relational Queries.

Claudio Sacerdoti Coen, Riccardo Treglia

Proceedings of the 24th Italian Conference on Theoretical Computer Science, 2023

2022

Reversibility in Erlang: Imperative Constructs.

Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, Giovanni Fabbretti

Proceedings of the Reversible Computation - 14th International Conference, 2022

2021

Strong Call-by-Value is Reasonable, Implosively.

Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Pre-Proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020).

Michael Hanus, Claudio Sacerdoti Coen

CoRR, 2020

Logic-Independent Proof Search in Logical Frameworks - (Short Paper).

Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Implementing type theory in higher order constraint logic programming.

Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi

Math. Struct. Comput. Sci., 2019

Sharing Equality is Linear.

Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

Crumbling Abstract Machines.

Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

Relational Data Across Mathematical Libraries.

Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

A Plugin to Export Coq Libraries to XML.

Claudio Sacerdoti Coen

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

The Coq Library as a Theory Graph.

Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

On the Prediction of Smart Contracts' Behaviours.

Cosimo Laneve, Claudio Sacerdoti Coen, Adele Veschetti

Proceedings of the From Software Engineering to Formal Methods and Tools, and Back, 2019

2018

Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper).

Alberto Fiori, Claudio Sacerdoti Coen

Proceedings of the Joint Proceedings of the CME-EI, 2018

2016

Implementing HOL in an Higher Order Logic Programming Language.

Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi

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

2015

A Survey on Retrieval of Mathematical Knowledge.

Ferruccio Guidi, Claudio Sacerdoti Coen

Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

ELPI: Fast, Embeddable, λProlog Interpreter.

Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi

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

On the Relative Usefulness of Fireballs.

Beniamino Accattoli, Claudio Sacerdoti Coen

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014

Matita Tutorial.

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen

J. Formaliz. Reason., 2014

On the Value of Variables.

Beniamino Accattoli, Claudio Sacerdoti Coen

Proceedings of the Logic, Language, Information, and Computation, 2014

On the Correctness of a Branch Displacement Algorithm.

Jaap Boender, Claudio Sacerdoti Coen

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

2013

Certified Complexity (CerCo).

Roberto M. Amadio, Nicholas Ayache, François Bobot, Jaap Boender, Brian Campbell, Ilias Garnier, Antoine Madet, James McKinna, Dominic P. Mulligan, Mauro Piccolo, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark, Paolo Tranquilli

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2013

2012

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

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

J. Autom. Reason., 2012

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

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

Log. Methods Comput. Sci., 2012

Lebesgue's dominated convergence theorem in Bishop's style.

Claudio Sacerdoti Coen, Enrico Zoli

Ann. Pure Appl. Log., 2012

A Term Rewriting System for Kuratowski's Closure-Complement Problem.

Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, Volker Sorge

Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , 2012

On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor.

Dominic P. Mulligan, Claudio Sacerdoti Coen

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Certified Complexity.

R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark

Proceedings of the 2nd European Future Technologies Conference and Exhibition, 2011

Formalising Overlap Algebras in Matita.

Claudio Sacerdoti Coen, Enrico Tassi

Math. Struct. Comput. Sci., 2011

A Foundational View on Integration Problems.

Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.

Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

The Matita Interactive Theorem Prover.

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

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

2010

Declarative Representation of Proof Terms.

Claudio Sacerdoti Coen

J. Autom. Reason., 2010

Preface.

David Aspinall, Claudio Sacerdoti Coen

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Regular Expressions, au point

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi

CoRR, 2010

Functions as Processes: Termination and the lm[(m)\tilde]\lambda\mu\widetilde{\mu}-Calculus.

Matteo Cimini, Claudio Sacerdoti Coen, Davide Sangiorgi

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

General Recursion and Formal Topology.

Claudio Sacerdoti Coen, Silvio Valentini

Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010

Some Considerations on the Usability of Interactive Provers.

Andrea Asperti, Claudio Sacerdoti Coen

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

2009

Nonuniform Coercions via Unification Hints

Claudio Sacerdoti Coen, Enrico Tassi

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

Hints in Unification.

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

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

Natural Deduction Environment for Matita.

Claudio Sacerdoti Coen, Enrico Tassi

Proceedings of the Intelligent Computer Mathematics, 2009

2008

Spurious Disambiguation Errors and How to Get Rid of Them.

Claudio Sacerdoti Coen, Stefano Zacchiroli

Math. Comput. Sci., 2008

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

Claudio Sacerdoti Coen, Enrico Tassi

J. Formaliz. Reason., 2008

A User Interface for a Mathematical System that Allows Ambiguous Formulae.

Claudio Sacerdoti Coen

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

2007

User Interaction with the Matita Proof Assistant.

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

J. Autom. Reason., 2007

Working with Mathematical Structures in Type Theory.

Claudio Sacerdoti Coen, Enrico Tassi

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

Spurious Disambiguation Error Detection.

Claudio Sacerdoti Coen, Stefano Zacchiroli

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

2006

Tinycals: Step by Step Tacticals.

Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

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

Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I.

Claudio Sacerdoti Coen

Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming, 2006

Crafting a Proof Assistant.

Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

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

A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus.

Serge Autexier, Claudio Sacerdoti Coen

Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

2005

Explanation in Natural Language of lamda-µµ-Terms.

Claudio Sacerdoti Coen

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

An Interactive Algebra Course with Formalised Proofs and Definitions.

Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004

Knowledge management of formal mathematics and interactive theorem proving.

Claudio Sacerdoti Coen

PhD thesis, 2004

Schemapath, a minimal extension to xml schema for conditional constraints.

Claudio Sacerdoti Coen, Paolo Marinelli, Fabio Vitali

Proceedings of the 13th international conference on World Wide Web, 2004

A Semi-reflexive Tactic for (Sub-)Equational Reasoning.

Claudio Sacerdoti Coen

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

A Content Based Mathematical Search Engine: Whelp.

Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli

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

Efficient Ambiguous Parsing of Mathematical Formulae.

Claudio Sacerdoti Coen, Stefano Zacchiroli

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

Mathematical Libraries as Proof Assistant Environments.

Claudio Sacerdoti Coen

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

A Generative Approach to the Implementation of Language Bindings for the Document Object Model.

Luca Padovani, Claudio Sacerdoti Coen, Stefano Zacchiroli

Proceedings of the Generative Programming and Component Engineering: Third International Conference, 2004

2003

Mathematical Knowledge Management in HELM.

Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi, Irene Schena

Ann. Math. Artif. Intell., 2003

From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls.

Claudio Sacerdoti Coen

Proceedings of the Mathematical Knowledge Management, Second International Conference, 2003

A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics.

Claudio Sacerdoti Coen

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2001

HELM and the Semantic Math-Web.

Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

XML, Stylesheets and the Re-mathematization of Formal Content.

Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena

Proceedings of the Extreme Markup Languages® 2001 Conference, 2001