XML, Stylesheets and the Re-mathematization of Formal Content. - Andrea Asperti; Luca Padovani; Claudio Sacerdoti Coen; Irene Schena (Extreme Markup Languages®, 2001)

HELM and the Semantic Math-Web. - Andrea Asperti; Luca Padovani; Claudio Sacerdoti Coen; Irene Schena (TPHOLs, 2001)

A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics. - Claudio Sacerdoti Coen (ICTCS, 2003)

From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. - Claudio Sacerdoti Coen (MKM, 2003)

Mathematical Knowledge Management in HELM. - Andrea Asperti; Luca Padovani; Claudio Sacerdoti Coen; Ferruccio Guidi; Irene Schena (Ann. Math. Artif. Intell., 2003)

A Generative Approach to the Implementation of Language Bindings for the Document Object Model. - Luca Padovani; Claudio Sacerdoti Coen; Stefano Zacchiroli (GPCE, 2004)

Mathematical Libraries as Proof Assistant Environments. - Claudio Sacerdoti Coen (MKM, 2004)

Efficient Ambiguous Parsing of Mathematical Formulae. - Claudio Sacerdoti Coen; Stefano Zacchiroli (MKM, 2004)

A Content Based Mathematical Search Engine: Whelp. - Andrea Asperti; Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (TYPES, 2004)

A Semi-reflexive Tactic for (Sub-)Equational Reasoning. - Claudio Sacerdoti Coen (TYPES, 2004)

Schemapath, a minimal extension to xml schema for conditional constraints. - Claudio Sacerdoti Coen; Paolo Marinelli; Fabio Vitali (WWW, 2004)

Knowledge management of formal mathematics and interactive theorem proving. - Claudio Sacerdoti Coen (2004)

An Interactive Algebra Course with Formalised Proofs and Definitions. - Andrea Asperti; Herman Geuvers; Iris Loeb; Lionel Elie Mamane; Claudio Sacerdoti Coen (MKM, 2005)

Explanation in Natural Language of lamda-µµ-Terms. - Claudio Sacerdoti Coen (MKM, 2005)

A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus. - Serge Autexier; Claudio Sacerdoti Coen (MKM, 2006)

Crafting a Proof Assistant. - Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (TYPES, 2006)

Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I. - Claudio Sacerdoti Coen (WRS@FLoC, 2006)

Tinycals: Step by Step Tacticals. - Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (UITP@FLoC, 2006)

Spurious Disambiguation Error Detection. - Claudio Sacerdoti Coen; Stefano Zacchiroli (Calculemus/MKM, 2007)

Working with Mathematical Structures in Type Theory. - Claudio Sacerdoti Coen; Enrico Tassi (TYPES, 2007)

User Interaction with the Matita Proof Assistant. - Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi; Stefano Zacchiroli (J. Autom. Reason., 2007)

A User Interface for a Mathematical System that Allows Ambiguous Formulae. - Claudio Sacerdoti Coen (UITP@TPHOLs, 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)

Spurious Disambiguation Errors and How to Get Rid of Them. - Claudio Sacerdoti Coen; Stefano Zacchiroli (Math. Comput. Sci., 2008)

Natural Deduction Environment for Matita. - Claudio Sacerdoti Coen; Enrico Tassi (Calculemus/MKM, 2009)

Hints in Unification. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (TPHOLs, 2009)

Nonuniform Coercions via Unification Hints - Claudio Sacerdoti Coen; Enrico Tassi (TYPES, 2009)

Some Considerations on the Usability of Interactive Provers. - Andrea Asperti; Claudio Sacerdoti Coen (AISC/MKM/Calculemus, 2010)

Functions as Processes: Termination and the lm[(m) tilde] lambda mu widetilde{ mu}-Calculus. - Matteo Cimini; Claudio Sacerdoti Coen; Davide Sangiorgi (TGC, 2010)

Regular Expressions, au point - Andrea Asperti; Claudio Sacerdoti Coen; Enrico Tassi (CoRR, 2010)

General Recursion and Formal Topology - Claudio Sacerdoti Coen; Silvio Valentini (PAR, 2010)

Preface. - David Aspinall 001; Claudio Sacerdoti Coen (UITP, 2010)

Declarative Representation of Proof Terms. - Claudio Sacerdoti Coen (J. Autom. Reason., 2010)

The Matita Interactive Theorem Prover. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (CADE, 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 (Calculemus/MKM, 2011)

A Foundational View on Integration Problems. - Florian Rabe 001; Michael Kohlhase; Claudio Sacerdoti Coen (Calculemus/MKM, 2011)

Formalising Overlap Algebras in Matita. - Claudio Sacerdoti Coen; Enrico Tassi (Math. Struct. Comput. Sci., 2011)

Certified Complexity. - R. Armadio; Andrea Asperti; Nicholas Ayache; Brian Campbell 001; Dominic P. Mulligan; Randy Pollack; Yann Régis-Gianas; Claudio Sacerdoti Coen; Ian Stark (FET, 2011)

On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. - Dominic P. Mulligan; Claudio Sacerdoti Coen (CPP, 2012)

A Term Rewriting System for Kuratowski's Closure-Complement Problem. - Osama Al-Hassani; Quratul-ain Mahesar; Claudio Sacerdoti Coen; Volker Sorge (RTA, 2012)

Lebesgue's dominated convergence theorem in Bishop's style. - Claudio Sacerdoti Coen; Enrico Zoli (Ann. Pure Appl. Log., 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)

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen; Enrico Tassi (J. Autom. Reason., 2012)

Certified Complexity (CerCo). - Roberto M. Amadio; Nicholas Ayache; François Bobot; Jaap Boender; Brian Campbell 001; Ilias Garnier; Antoine Madet; James McKinna; Dominic P. Mulligan; Mauro Piccolo; Randy Pollack; Yann Régis-Gianas; et al. (FOPARA, 2013)

On the Correctness of a Branch Displacement Algorithm. - Jaap Boender; Claudio Sacerdoti Coen (TACAS, 2014)

Matita Tutorial. - Andrea Asperti; Wilmer Ricciotti; Claudio Sacerdoti Coen (J. Formaliz. Reason., 2014)

On the Relative Usefulness of Fireballs. - Beniamino Accattoli; Claudio Sacerdoti Coen (LICS, 2015)

ELPI: Fast, Embeddable, λProlog Interpreter. - Cvetan Dunchev; Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi (LPAR, 2015)

Implementing HOL in an Higher Order Logic Programming Language. - Cvetan Dunchev; Claudio Sacerdoti Coen; Enrico Tassi (LFMTP, 2016)

A Survey on Retrieval of Mathematical Knowledge. - Ferruccio Guidi; Claudio Sacerdoti Coen (Math. Comput. Sci., 2016)

On the value of variables. - Beniamino Accattoli; Claudio Sacerdoti Coen (Inf. Comput., 2017)

Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper). - Alberto Fiori; Claudio Sacerdoti Coen (CICM Workshops, 2018)

On the Prediction of Smart Contracts' Behaviours. - Cosimo Laneve; Claudio Sacerdoti Coen; Adele Veschetti (From Software Engineering to Formal Methods and Tools, and Back, 2019)

The Coq Library as a Theory Graph. - Dennis Müller 001; Florian Rabe 001; Claudio Sacerdoti Coen (CICM, 2019)

A Plugin to Export Coq Libraries to XML. - Claudio Sacerdoti Coen (CICM, 2019)

Relational Data Across Mathematical Libraries. - Andrea Condoluci; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001; Claudio Sacerdoti Coen; Makarius Wenzel (CICM, 2019)

Crumbling Abstract Machines. - Beniamino Accattoli; Andrea Condoluci; Giulio Guerrieri; Claudio Sacerdoti Coen (PPDP, 2019)

Sharing Equality is Linear. - Andrea Condoluci; Beniamino Accattoli; Claudio Sacerdoti Coen (PPDP, 2019)

Implementing type theory in higher order constraint logic programming. - Ferruccio Guidi; Claudio Sacerdoti Coen; Enrico Tassi (Math. Struct. Comput. Sci., 2019)

Logic-Independent Proof Search in Logical Frameworks - (Short Paper). - Michael Kohlhase; Florian Rabe 001; Claudio Sacerdoti Coen; Jan Frederik Schaefer (IJCAR (1), 2020)

Pre-Proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020). - Michael Hanus; Claudio Sacerdoti Coen (CoRR, 2020)

Strong Call-by-Value is Reasonable, Implosively. - Beniamino Accattoli; Andrea Condoluci; Claudio Sacerdoti Coen (LICS, 2021)

Reversibility in Erlang: Imperative Constructs. - Pietro Lami; Ivan Lanese; Jean-Bernard Stefani; Claudio Sacerdoti Coen; Giovanni Fabbretti (RC, 2022)

Properties of a Computational Lambda Calculus for Higher-Order Relational Queries. - Claudio Sacerdoti Coen; Riccardo Treglia (ICTCS, 2023)

Formalizing Functions as Processes. - Beniamino Accattoli; Horace Blanc; Claudio Sacerdoti Coen (ITP, 2023)

Causal Reversibility Implies Time Reversibility. - Marco Bernardo 001; Ivan Lanese; Andrea Marin; Claudio Antares Mezzina; Sabina Rossi; Claudio Sacerdoti Coen (QEST, 2023)

IMELL Cut Elimination with Linear Overhead. - Beniamino Accattoli; Claudio Sacerdoti Coen (FSCD, 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)

sesame. - Claudio Sacerdoti Coen (DROPS Artifacts, 2024)

The Cost of Skeletal Call-By-Need, Smoothly. - Beniamino Accattoli; Francesco Magliocca; Loïc Peyrot; Claudio Sacerdoti Coen (FSCD, 2025)

Positive Sharing and Abstract Machines. - Beniamino Accattoli; Claudio Sacerdoti Coen; Jui-Hsuan Wu (CoRR, 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, 2025)

Thinking Machines: Mathematical Reasoning in the Age of LLMs. - Andrea Asperti; Alberto Naibo; Claudio Sacerdoti Coen (CoRR, 2025)