default search action
Claudio Sacerdoti Coen
Person information
- affiliation: University of Bologna, Italy
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j14]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: 100944 (2024) - [c54]Beniamino Accattoli, Claudio Sacerdoti Coen:
IMELL Cut Elimination with Linear Overhead. FSCD 2024: 24:1-24:24 - [e10]Florian Rabe, Claudio Sacerdoti Coen:
Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024. EPTCS 404, 2024 [contents] - [i10]Beniamino Accattoli, Claudio Sacerdoti Coen:
IMELL Cut Elimination with Linear Overhead. CoRR abs/2405.03669 (2024) - 2023
- [c53]Claudio Sacerdoti Coen, Riccardo Treglia:
Properties of a Computational Lambda Calculus for Higher-Order Relational Queries. ICTCS 2023: 254-267 - [c52]Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen:
Formalizing Functions as Processes. ITP 2023: 5:1-5:21 - [c51]Marco Bernardo, Ivan Lanese, Andrea Marin, Claudio Antares Mezzina, Sabina Rossi, Claudio Sacerdoti Coen:
Causal Reversibility Implies Time Reversibility. QEST 2023: 270-287 - [e9]Jasmin Blanchette, James H. Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Müller, Yasmine Sharoda, Claudio Sacerdoti Coen:
Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26 - 31, 2021. CEUR Workshop Proceedings 3377, CEUR-WS.org 2023 [contents] - 2022
- [c50]Pietro Lami
Reversibility in Erlang: Imperative Constructs. RC 2022: 187-203 - [e8]Claudio Sacerdoti Coen, Ivano Salvo:
Proceedings of the 22nd Italian Conference on Theoretical Computer Science, Bologna, Italy, September 13-15, 2021. CEUR Workshop Proceedings 3072, CEUR-WS.org 2022 [contents] - 2021
- [c49]Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen:
Strong Call-by-Value is Reasonable, Implosively. LICS 2021: 1-14 - [e7]Fairouz Kamareddine, Claudio Sacerdoti Coen
Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings. Lecture Notes in Computer Science 12833, Springer 2021, ISBN 978-3-030-81096-2 [contents] - [e6]Michael Hanus
Functional and Constraint Logic Programming - 28th International Workshop, WFLP 2020, Bologna, Italy, September 7, 2020, Revised Selected Papers. Lecture Notes in Computer Science 12560, Springer 2021, ISBN 978-3-030-75332-0 [contents] - [e5]Claudio Sacerdoti Coen, Alwen Tiu:
Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020. EPTCS 332, 2021 [contents] - [i9]Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen:
Strong Call-by-Value is Reasonable, Implosively. CoRR abs/2102.06928 (2021) - 2020
- [c48]Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer:
Logic-Independent Proof Search in Logical Frameworks - (Short Paper). IJCAR (1) 2020: 395-401 - [e4]Edwin C. Brady, James H. Davenport, William M. Farmer, Cezary Kaliszyk, Andrea Kohlhase, Michael Kohlhase, Dennis Müller, Karol Pak, Claudio Sacerdoti Coen:
Joint Proceedings of the FMM and LML Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2019 co-located with the 12th Conference on Intelligent Computer Mathematics (CICM 2019), Prague, Czech Republic, July 8-12, 2019. CEUR Workshop Proceedings 2634, CEUR-WS.org 2020 [contents] - [i8]Michael Hanus, Claudio Sacerdoti Coen:
Pre-Proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020). CoRR abs/2009.01001 (2020)
2010 – 2019
- 2019
- [j13]Ferruccio Guidi
Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. 29(8): 1125-1150 (2019) - [c47]Cosimo Laneve
On the Prediction of Smart Contracts' Behaviours. From Software Engineering to Formal Methods and Tools, and Back 2019: 397-415 - [c46]Andrea Condoluci
Relational Data Across Mathematical Libraries. CICM 2019: 61-76 - [c45]Dennis Müller
The Coq Library as a Theory Graph. CICM 2019: 171-186 - [c44]Claudio Sacerdoti Coen:
A Plugin to Export Coq Libraries to XML. CICM 2019: 243-257 - [c43]Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri
Crumbling Abstract Machines. PPDP 2019: 4:1-4:15 - [c42]Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen:
Sharing Equality is Linear. PPDP 2019: 9:1-9:14 - [e3]Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, Claudio Sacerdoti Coen:
Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings. Lecture Notes in Computer Science 11617, Springer 2019, ISBN 978-3-030-23249-8 [contents] - [i7]Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen:
Crumbling Abstract Machines. CoRR abs/1907.06057 (2019) - [i6]Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen:
Sharing Equality is Linear. CoRR abs/1907.06101 (2019) - 2018
- [c41]Alberto Fiori, Claudio Sacerdoti Coen:
Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper). CICM Workshops 2018 - 2017
- [j12]Beniamino Accattoli, Claudio Sacerdoti Coen
On the value of variables. Inf. Comput. 255: 224-242 (2017) - 2016
- [j11]Ferruccio Guidi
A Survey on Retrieval of Mathematical Knowledge. Math. Comput. Sci. 10(4): 409-427 (2016) - [c40]Cvetan Dunchev, Claudio Sacerdoti Coen
Implementing HOL in an Higher Order Logic Programming Language. LFMTP 2016: 4:1-4:10 - 2015
- [c39]Beniamino Accattoli, Claudio Sacerdoti Coen
On the Relative Usefulness of Fireballs. LICS 2015: 141-155 - [c38]Cvetan Dunchev, Ferruccio Guidi
ELPI: Fast, Embeddable, λProlog Interpreter. LPAR 2015: 460-468 - [c37]Ferruccio Guidi
A Survey on Retrieval of Mathematical Knowledge. CICM 2015: 296-315 - [i5]Beniamino Accattoli, Claudio Sacerdoti Coen:
On the Relative Usefulness of Fireballs. CoRR abs/1505.03791 (2015) - [i4]Ferruccio Guidi, Claudio Sacerdoti Coen:
A Survey on Retrieval of Mathematical Knowledge. CoRR abs/1505.06646 (2015) - 2014
- [j10]Andrea Asperti
Matita Tutorial. J. Formaliz. Reason. 7(2): 91-199 (2014) - [c36]Jaap Boender, Claudio Sacerdoti Coen
On the Correctness of a Branch Displacement Algorithm. TACAS 2014: 605-619 - [c35]Beniamino Accattoli, Claudio Sacerdoti Coen
On the Value of Variables. WoLLIC 2014: 36-50 - 2013
- [c34]Roberto M. Amadio, Nicholas Ayache, François Bobot
Certified Complexity (CerCo). FOPARA 2013: 1-18 - 2012
- [j9]Claudio Sacerdoti Coen
Lebesgue's dominated convergence theorem in Bishop's style. Ann. Pure Appl. Log. 163(2): 140-150 (2012) - [j8]Andrea Asperti
A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Log. Methods Comput. Sci. 8(1) (2012) - [j7]Andrea Asperti
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. J. Autom. Reason. 49(3): 427-451 (2012) - [c33]Dominic P. Mulligan
On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. CPP 2012: 43-59 - [c32]Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen
A Term Rewriting System for Kuratowski's Closure-Complement Problem. RTA 2012: 38-52 - [e2]David Aspinall, Claudio Sacerdoti Coen:
Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, UITP 2010, Edinburgh, UK, July 15, 2010. Electronic Notes in Theoretical Computer Science 285, Elsevier 2012 [contents] - [i3]Jaap Boender, Claudio Sacerdoti Coen:
On the correctness of a branch displacement algorithm. CoRR abs/1209.5920 (2012) - 2011
- [j6]Claudio Sacerdoti Coen
Formalising Overlap Algebras in Matita. Math. Struct. Comput. Sci. 21(4): 763-793 (2011) - [c31]Andrea Asperti
The Matita Interactive Theorem Prover. CADE 2011: 64-69 - [c30]Florian Rabe
A Foundational View on Integration Problems. Calculemus/MKM 2011: 107-122 - [c29]Andrea Asperti
Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. Calculemus/MKM 2011: 278-280 - [c28]R. Armadio, Andrea Asperti
Certified Complexity. FET 2011: 175-177 - [i2]Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen:
A Foundational View on Integration Problems. CoRR abs/1105.2725 (2011) - 2010
- [j5]Claudio Sacerdoti Coen
Declarative Representation of Proof Terms. J. Autom. Reason. 44(1-2): 25-52 (2010) - [c27]Andrea Asperti
Some Considerations on the Usability of Interactive Provers. AISC/MKM/Calculemus 2010: 147-156 - [c26]Claudio Sacerdoti Coen, Silvio Valentini:
General Recursion and Formal Topology. PAR@ITP 2010: 72-83 - [c25]Matteo Cimini, Claudio Sacerdoti Coen
Functions as Processes: Termination and the lm[(m)\tilde]\lambda\mu\widetilde{\mu}-Calculus. TGC 2010: 73-86 - [c24]Claudio Sacerdoti Coen, Silvio Valentini:
General Recursion and Formal Topology. PAR 2010: 65-75 - [c23]David Aspinall, Claudio Sacerdoti Coen
Preface. UITP 2010: 1-2 - [i1]Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi:
Regular Expressions, au point. CoRR abs/1010.2604 (2010)
2000 – 2009
- 2009
- [c22]Claudio Sacerdoti Coen
Natural Deduction Environment for Matita. Calculemus/MKM 2009: 486-491 - [c21]Andrea Asperti
Hints in Unification. TPHOLs 2009: 84-98 - [c20]Claudio Sacerdoti Coen
Nonuniform Coercions via Unification Hints. TYPES 2009: 16-29 - [e1]Jacques Carette
Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings. Lecture Notes in Computer Science 5625, Springer 2009, ISBN 978-3-642-02613-3 [contents] - 2008
- [j4]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): 51-89 (2008) - [j3]Claudio Sacerdoti Coen
Spurious Disambiguation Errors and How to Get Rid of Them. Math. Comput. Sci. 2(2): 355-378 (2008) - [c19]Claudio Sacerdoti Coen
A User Interface for a Mathematical System that Allows Ambiguous Formulae. UITP@TPHOLs 2008: 67-87 - 2007
- [j2]Andrea Asperti
User Interaction with the Matita Proof Assistant. J. Autom. Reason. 39(2): 109-139 (2007) - [c18]Claudio Sacerdoti Coen, Stefano Zacchiroli
Spurious Disambiguation Error Detection. Calculemus/MKM 2007: 381-392 - [c17]Claudio Sacerdoti Coen
Working with Mathematical Structures in Type Theory. TYPES 2007: 157-172 - 2006
- [c16]Serge Autexier
A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus. MKM 2006: 67-81 - [c15]Andrea Asperti
Crafting a Proof Assistant. TYPES 2006: 18-32 - [c14]Claudio Sacerdoti Coen
Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I. WRS@FLoC 2006: 97-118 - [c13]Claudio Sacerdoti Coen
Tinycals: Step by Step Tacticals. UITP@FLoC 2006: 125-142 - 2005
- [c12]Claudio Sacerdoti Coen
Explanation in Natural Language of lamda-µµ-Terms. MKM 2005: 234-249 - [c11]Andrea Asperti
An Interactive Algebra Course with Formalised Proofs and Definitions. MKM 2005: 315-329 - 2004
- [b1]Claudio Sacerdoti Coen:
Knowledge management of formal mathematics and interactive theorem proving. University of Bologna, Italy, 2004 - [c10]Luca Padovani, Claudio Sacerdoti Coen, Stefano Zacchiroli:
A Generative Approach to the Implementation of Language Bindings for the Document Object Model. GPCE 2004: 469-487 - [c9]Claudio Sacerdoti Coen:
Mathematical Libraries as Proof Assistant Environments. MKM 2004: 332-346 - [c8]Claudio Sacerdoti Coen, Stefano Zacchiroli:
Efficient Ambiguous Parsing of Mathematical Formulae. MKM 2004: 347-362 - [c7]Andrea Asperti
A Content Based Mathematical Search Engine: Whelp. TYPES 2004: 17-32 - [c6]Claudio Sacerdoti Coen:
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. TYPES 2004: 98-114 - [c5]Claudio Sacerdoti Coen, Paolo Marinelli, Fabio Vitali:
Schemapath, a minimal extension to xml schema for conditional constraints. WWW 2004: 164-174 - 2003
- [j1]Andrea Asperti
Mathematical Knowledge Management in HELM. Ann. Math. Artif. Intell. 38(1-3): 27-46 (2003) - [c4]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: 37-57 - [c3]Claudio Sacerdoti Coen:
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. MKM 2003: 30-44 - 2001
- [c2]Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena:
XML, Stylesheets and the Re-mathematization of Formal Content. Extreme Markup Languages® 2001 - [c1]Andrea Asperti
HELM and the Semantic Math-Web. TPHOLs 2001: 59-74
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-04 21:44 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: