Claudio Sacerdoti Coen

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 25

Top Topics

Logic Programming

Higher Order Logic

Relational Queries

Top Venues

Publications

Florian Rabe, Claudio Sacerdoti Coen
Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. CoRR (2024)
Beniamino Accattoli, Claudio Sacerdoti Coen
IMELL Cut Elimination with Linear Overhead. FSCD (2024)
Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, Giovanni Fabbretti
Reversible debugging of concurrent Erlang programs: Supporting imperative primitives. J. Log. Algebraic Methods Program. 138 (2024)
Beniamino Accattoli, Claudio Sacerdoti Coen
IMELL Cut Elimination with Linear Overhead. CoRR (2024)
Claudio Sacerdoti Coen, Riccardo Treglia
Properties of a Computational Lambda Calculus for Higher-Order Relational Queries. ICTCS (2023)
Marco Bernardo, Ivan Lanese, Andrea Marin, Claudio Antares Mezzina, Sabina Rossi, Claudio Sacerdoti Coen
Causal Reversibility Implies Time Reversibility. QEST (2023)
Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen
Formalizing Functions as Processes. ITP (2023)
Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, Giovanni Fabbretti
Reversibility in Erlang: Imperative Constructs. RC (2022)
Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
Strong Call-by-Value is Reasonable, Implosively. CoRR (2021)
Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
Strong Call-by-Value is Reasonable, Implosively. LICS (2021)
Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer
Logic-Independent Proof Search in Logical Frameworks - (Short Paper). IJCAR (1) (2020)
Michael Hanus, Claudio Sacerdoti Coen
Pre-Proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020). CoRR (2020)
Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. 29 (8) (2019)
Claudio Sacerdoti Coen
A Plugin to Export Coq Libraries to XML. CICM (2019)
Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
Sharing Equality is Linear. PPDP (2019)
Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel
Relational Data Across Mathematical Libraries. CICM (2019)
Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
Crumbling Abstract Machines. CoRR (2019)
Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
Crumbling Abstract Machines. PPDP (2019)
Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
Sharing Equality is Linear. CoRR (2019)
Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen
The Coq Library as a Theory Graph. CICM (2019)
Cosimo Laneve, Claudio Sacerdoti Coen, Adele Veschetti
On the Prediction of Smart Contracts' Behaviours. From Software Engineering to Formal Methods and Tools, and Back (2019)
Alberto Fiori, Claudio Sacerdoti Coen
Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper). CICM Workshops (2018)
Beniamino Accattoli, Claudio Sacerdoti Coen
On the value of variables. Inf. Comput. 255 (2017)
Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
Implementing HOL in an Higher Order Logic Programming Language. LFMTP (2016)
Ferruccio Guidi, Claudio Sacerdoti Coen
A Survey on Retrieval of Mathematical Knowledge. Math. Comput. Sci. 10 (4) (2016)
Beniamino Accattoli, Claudio Sacerdoti Coen
On the Relative Usefulness of Fireballs. LICS (2015)
Ferruccio Guidi, Claudio Sacerdoti Coen
A Survey on Retrieval of Mathematical Knowledge. CoRR (2015)
Ferruccio Guidi, Claudio Sacerdoti Coen
A Survey on Retrieval of Mathematical Knowledge. CICM (2015)
Beniamino Accattoli, Claudio Sacerdoti Coen
On the Relative Usefulness of Fireballs. CoRR (2015)
Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
ELPI: Fast, Embeddable, \lambda Prolog Interpreter. LPAR (2015)
Beniamino Accattoli, Claudio Sacerdoti Coen
On the Value of Variables. WoLLIC (2014)
Jaap Boender, Claudio Sacerdoti Coen
On the Correctness of a Branch Displacement Algorithm. TACAS (2014)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen
Matita Tutorial. J. Formaliz. Reason. 7 (2) (2014)
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
Certified Complexity (CerCo). FOPARA (2013)
Dominic P. Mulligan, Claudio Sacerdoti Coen
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. CPP (2012)
David Aspinall, Claudio Sacerdoti Coen
Preface. Electron. Notes Theor. Comput. Sci. 285 (2012)
Jaap Boender, Claudio Sacerdoti Coen
On the correctness of a branch displacement algorithm CoRR (2012)
Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, Volker Sorge
A Term Rewriting System for Kuratowski's Closure-Complement Problem. RTA (2012)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. J. Autom. Reason. 49 (3) (2012)
Claudio Sacerdoti Coen, Enrico Zoli
Lebesgue's dominated convergence theorem in Bishop's style. Ann. Pure Appl. Log. 163 (2) (2012)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions Log. Methods Comput. Sci. 8 (1) (2012)
Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
A Foundational View on Integration Problems. Calculemus/MKM (2011)
Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
A Foundational View on Integration Problems CoRR (2011)
Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. Calculemus/MKM (2011)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
The Matita Interactive Theorem Prover. CADE (2011)
R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark
Certified Complexity. FET (2011)
Claudio Sacerdoti Coen, Enrico Tassi
Formalising Overlap Algebras in Matita. Math. Struct. Comput. Sci. 21 (4) (2011)
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
Regular Expressions, au point CoRR (2010)
Matteo Cimini, Claudio Sacerdoti Coen, Davide Sangiorgi
Functions as Processes: Termination and the lm[(m)\tilde]\lambda\mu\widetilde{\mu}-Calculus. TGC (2010)
Andrea Asperti, Claudio Sacerdoti Coen
Some Considerations on the Usability of Interactive Provers. AISC/MKM/Calculemus (2010)
Claudio Sacerdoti Coen, Silvio Valentini
General Recursion and Formal Topology PAR (2010)
Claudio Sacerdoti Coen, Silvio Valentini
General Recursion and Formal Topology. PAR@ITP (2010)
Claudio Sacerdoti Coen
Declarative Representation of Proof Terms. J. Autom. Reason. 44 (1-2) (2010)
Claudio Sacerdoti Coen
A User Interface for a Mathematical System that Allows Ambiguous Formulae. Electron. Notes Theor. Comput. Sci. 226 (2009)
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
Hints in Unification. TPHOLs (2009)
Claudio Sacerdoti Coen, Enrico Tassi
Natural Deduction Environment for Matita. Calculemus/MKM (2009)
Claudio Sacerdoti Coen, Enrico Tassi
Nonuniform Coercions via Unification Hints TYPES (2009)
Claudio Sacerdoti Coen, Enrico Tassi
A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita. J. Formaliz. Reason. 1 (1) (2008)
Claudio Sacerdoti Coen, Stefano Zacchiroli
Spurious Disambiguation Errors and How to Get Rid of Them. Math. Comput. Sci. 2 (2) (2008)
Claudio Sacerdoti Coen, Enrico Tassi
Working with Mathematical Structures in Type Theory. TYPES (2007)
Claudio Sacerdoti Coen, Stefano Zacchiroli
Spurious Disambiguation Error Detection. Calculemus/MKM (2007)
Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Tinycals: Step by Step Tacticals. Electron. Notes Theor. Comput. Sci. 174 (2) (2007)
Claudio Sacerdoti Coen
Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I. Electron. Notes Theor. Comput. Sci. 174 (10) (2007)
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
User Interaction with the Matita Proof Assistant. J. Autom. Reason. 39 (2) (2007)
Serge Autexier, Claudio Sacerdoti Coen
A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus. MKM (2006)
Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
Crafting a Proof Assistant. TYPES (2006)
Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen
An Interactive Algebra Course with Formalised Proofs and Definitions. MKM (2005)
Claudio Sacerdoti Coen
Explanation in Natural Language of lamda-µµ-Terms. MKM (2005)
Luca Padovani, Claudio Sacerdoti Coen, Stefano Zacchiroli
A Generative Approach to the Implementation of Language Bindings for the Document Object Model. GPCE (2004)
Claudio Sacerdoti Coen, Stefano Zacchiroli
Efficient Ambiguous Parsing of Mathematical Formulae. MKM (2004)
Claudio Sacerdoti Coen, Paolo Marinelli, Fabio Vitali
Schemapath, a minimal extension to xml schema for conditional constraints. WWW (2004)
Claudio Sacerdoti Coen
Mathematical Libraries as Proof Assistant Environments. MKM (2004)
Claudio Sacerdoti Coen
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. TYPES (2004)
Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
A Content Based Mathematical Search Engine: Whelp. TYPES (2004)
Claudio Sacerdoti Coen
A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics. ICTCS (2003)
Claudio Sacerdoti Coen
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. MKM (2003)
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi, Irene Schena
Mathematical Knowledge Management in HELM. Ann. Math. Artif. Intell. 38 (1-3) (2003)
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena
HELM and the Semantic Math-Web. TPHOLs (2001)
Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena
XML, Stylesheets and the Re-mathematization of Formal Content. Extreme Markup Languages® (2001)