Claudio Sacerdoti Coen

98 papers A* 3A 2B 7C 12Journal 29Unranked 36

Year	Rank	Type	Title / Venue / Authors
2025	C	`conf`	Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. PPDP Beniamino Accattoli, Cláudio Belo Lourenço, Dan R. Ghica, Giulio Guerrieri, Claudio Sacerdoti Coen
2025	J	`jnl`	Closure Conversion, Flat Environments, and the Complexity of Abstract Machines. CoRR Beniamino Accattoli, Dan R. Ghica, Giulio Guerrieri, Cláudio Belo Lourenço, Claudio Sacerdoti Coen
2025	C	`conf`	Indexing and Retrieval in a Heterogeneous Formal Library. CICM Claudio Sacerdoti Coen, Abdelghani Alidra
2025	B	`conf`	Positive Sharing and Abstract Machines. APLAS Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu
2025	J	`jnl`	Positive Sharing and Abstract Machines. CoRR Beniamino Accattoli, Claudio Sacerdoti Coen, Jui-Hsuan Wu
2025	B	`conf`	The Cost of Skeletal Call-By-Need, Smoothly. FSCD Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, Claudio Sacerdoti Coen
2025	J	`jnl`	The Cost of Skeletal Call-by-Need, Smoothly. CoRR Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, Claudio Sacerdoti Coen
2025	J	`jnl`	Thinking Machines: Mathematical Reasoning in the Age of LLMs. Big Data Cogn. Comput. Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen
2025	J	`jnl`	Thinking Machines: Mathematical Reasoning in the Age of LLMs. CoRR Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen
2024	B	`conf`	IMELL Cut Elimination with Linear Overhead. FSCD Beniamino Accattoli, Claudio Sacerdoti Coen
2024	J	`jnl`	IMELL Cut Elimination with Linear Overhead. CoRR Beniamino Accattoli, Claudio Sacerdoti Coen
2024	—	`ed.`	Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2024, Tallinn, Estonia, 8th July 2024. LFMTP@FSCD Florian Rabe, Claudio Sacerdoti Coen
2024	J	`jnl`	Reversible debugging of concurrent Erlang programs: Supporting imperative primitives. J. Log. Algebraic Methods Program. Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, Giovanni Fabbretti
2023	—	`conf`	Causal Reversibility Implies Time Reversibility. QEST Marco Bernardo, Ivan Lanese, Andrea Marin, Claudio Antares Mezzina, Sabina Rossi, Claudio Sacerdoti Coen
2023	B	`conf`	Formalizing Functions as Processes. ITP Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen
2023	—	`ed.`	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. CICM Workshops Jasmin Blanchette, James H. Davenport, Peter Koepke, Michael Kohlhase, Andrea Kohlhase, Adam Naumowicz, Dennis Müller, Yasmine Sharoda, Claudio Sacerdoti Coen
2023	—	`conf`	Properties of a Computational Lambda Calculus for Higher-Order Relational Queries. ICTCS Claudio Sacerdoti Coen, Riccardo Treglia
2022	—	`ed.`	Proceedings of the 22nd Italian Conference on Theoretical Computer Science, Bologna, Italy, September 13-15, 2021. ICTCS Claudio Sacerdoti Coen, Ivano Salvo
2022	C	`conf`	Reversibility in Erlang: Imperative Constructs. RC Pietro Lami, Ivan Lanese, Jean-Bernard Stefani, Claudio Sacerdoti Coen, Giovanni Fabbretti
2021	—	`ed.`	Functional and Constraint Logic Programming - 28th International Workshop, WFLP 2020, Bologna, Italy, September 7, 2020, Revised Selected Papers WFLP Michael Hanus, Claudio Sacerdoti Coen
2021	C	`ed.`	Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings CICM Fairouz Kamareddine, Claudio Sacerdoti Coen
2021	—	`ed.`	Proceedings Fifteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2020, Paris, France, 29th June 2020. LFMTP Claudio Sacerdoti Coen, Alwen Tiu
2021	A*	`conf`	Strong Call-by-Value is Reasonable, Implosively. LICS Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
2021	J	`jnl`	Strong Call-by-Value is Reasonable, Implosively. CoRR Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
2020	—	`ed.`	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. CICM Workshops Edwin C. Brady, James H. Davenport, William M. Farmer, Cezary Kaliszyk, Andrea Kohlhase, Michael Kohlhase, Dennis Müller, Karol Pak, Claudio Sacerdoti Coen
2020	—	`conf`	Logic-Independent Proof Search in Logical Frameworks - (Short Paper). IJCAR (1) Michael Kohlhase, Florian Rabe, Claudio Sacerdoti Coen, Jan Frederik Schaefer
2020	J	`jnl`	Pre-Proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020). CoRR Michael Hanus, Claudio Sacerdoti Coen
2019	C	`conf`	A Plugin to Export Coq Libraries to XML. CICM Claudio Sacerdoti Coen
2019	C	`conf`	Crumbling Abstract Machines. PPDP Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
2019	J	`jnl`	Crumbling Abstract Machines. CoRR Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
2019	J	`jnl`	Implementing type theory in higher order constraint logic programming. Math. Struct. Comput. Sci. Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
2019	C	`ed.`	Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings CICM Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, Claudio Sacerdoti Coen
2019	—	`conf`	On the Prediction of Smart Contracts' Behaviours. From Software Engineering to Formal Methods and Tools, and Back Cosimo Laneve, Claudio Sacerdoti Coen, Adele Veschetti
2019	C	`conf`	Relational Data Across Mathematical Libraries. CICM Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, Makarius Wenzel
2019	C	`conf`	Sharing Equality is Linear. PPDP Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
2019	J	`jnl`	Sharing Equality is Linear. CoRR Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
2019	C	`conf`	The Coq Library as a Theory Graph. CICM Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen
2018	—	`conf`	Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper). CICM Workshops Alberto Fiori, Claudio Sacerdoti Coen
2017	J	`jnl`	On the value of variables. Inf. Comput. Beniamino Accattoli, Claudio Sacerdoti Coen
2016	J	`jnl`	A Survey on Retrieval of Mathematical Knowledge. Math. Comput. Sci. Ferruccio Guidi, Claudio Sacerdoti Coen
2016	—	`conf`	Implementing HOL in an Higher Order Logic Programming Language. LFMTP Cvetan Dunchev, Claudio Sacerdoti Coen, Enrico Tassi
2015	C	`conf`	A Survey on Retrieval of Mathematical Knowledge. CICM Ferruccio Guidi, Claudio Sacerdoti Coen
2015	J	`jnl`	A Survey on Retrieval of Mathematical Knowledge. CoRR Ferruccio Guidi, Claudio Sacerdoti Coen
2015	B	`conf`	ELPI: Fast, Embeddable, λProlog Interpreter. LPAR Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi
2015	A*	`conf`	On the Relative Usefulness of Fireballs. LICS Beniamino Accattoli, Claudio Sacerdoti Coen
2015	J	`jnl`	On the Relative Usefulness of Fireballs. CoRR Beniamino Accattoli, Claudio Sacerdoti Coen
2014	J	`jnl`	Matita Tutorial. J. Formaliz. Reason. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen
2014	A	`conf`	On the Correctness of a Branch Displacement Algorithm. TACAS Jaap Boender, Claudio Sacerdoti Coen
2014	C	`conf`	On the Value of Variables. WoLLIC Beniamino Accattoli, Claudio Sacerdoti Coen
2013	—	`conf`	Certified Complexity (CerCo). FOPARA 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
2012	J	`jnl`	A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions Log. Methods Comput. Sci. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2012	—	`conf`	A Term Rewriting System for Kuratowski's Closure-Complement Problem. RTA Osama Al-Hassani, Quratul-ain Mahesar, Claudio Sacerdoti Coen, Volker Sorge
2012	J	`jnl`	Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover. J. Autom. Reason. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2012	J	`jnl`	Lebesgue's dominated convergence theorem in Bishop's style. Ann. Pure Appl. Log. Claudio Sacerdoti Coen, Enrico Zoli
2012	B	`conf`	On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor. CPP Dominic P. Mulligan, Claudio Sacerdoti Coen
2012	J	`jnl`	On the correctness of a branch displacement algorithm CoRR Jaap Boender, Claudio Sacerdoti Coen
2012	—	`ed.`	Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, UITP 2010, Edinburgh, UK, July 15, 2010 UITP David Aspinall, Claudio Sacerdoti Coen
2011	J	`jnl`	A Foundational View on Integration Problems CoRR Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
2011	—	`conf`	A Foundational View on Integration Problems. Calculemus/MKM Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
2011	—	`conf`	Certified Complexity. FET R. Armadio, Andrea Asperti, Nicholas Ayache, Brian Campbell, Dominic P. Mulligan, Randy Pollack, Yann Régis-Gianas, Claudio Sacerdoti Coen, Ian Stark
2011	J	`jnl`	Formalising Overlap Algebras in Matita. Math. Struct. Comput. Sci. Claudio Sacerdoti Coen, Enrico Tassi
2011	—	`conf`	Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita. Calculemus/MKM Andrea Asperti, Maria Emilia Maietti, Claudio Sacerdoti Coen, Giovanni Sambin, Silvio Valentini
2011	A	`conf`	The Matita Interactive Theorem Prover. CADE Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2010	J	`jnl`	Declarative Representation of Proof Terms. J. Autom. Reason. Claudio Sacerdoti Coen
2010	—	`conf`	Functions as Processes: Termination and the lm[(m)\tilde]\lambda\mu\widetilde{\mu}-Calculus. TGC Matteo Cimini, Claudio Sacerdoti Coen, Davide Sangiorgi
2010	—	`conf`	General Recursion and Formal Topology PAR Claudio Sacerdoti Coen, Silvio Valentini
2010	—	`conf`	General Recursion and Formal Topology. PAR@ITP Claudio Sacerdoti Coen, Silvio Valentini
2010	—	`conf`	Preface. UITP David Aspinall, Claudio Sacerdoti Coen
2010	J	`jnl`	Regular Expressions, au point CoRR Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
2010	—	`conf`	Some Considerations on the Usability of Interactive Provers. AISC/MKM/Calculemus Andrea Asperti, Claudio Sacerdoti Coen
2009	—	`conf`	Hints in Unification. TPHOLs Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi
2009	—	`ed.`	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 Calculemus/MKM Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt
2009	—	`conf`	Natural Deduction Environment for Matita. Calculemus/MKM Claudio Sacerdoti Coen, Enrico Tassi
2009	—	`conf`	Nonuniform Coercions via Unification Hints TYPES Claudio Sacerdoti Coen, Enrico Tassi
2008	—	`conf`	A User Interface for a Mathematical System that Allows Ambiguous Formulae. UITP@TPHOLs Claudio Sacerdoti Coen
2008	J	`jnl`	A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita. J. Formaliz. Reason. Claudio Sacerdoti Coen, Enrico Tassi
2008	J	`jnl`	Spurious Disambiguation Errors and How to Get Rid of Them. Math. Comput. Sci. Claudio Sacerdoti Coen, Stefano Zacchiroli
2007	—	`conf`	Spurious Disambiguation Error Detection. Calculemus/MKM Claudio Sacerdoti Coen, Stefano Zacchiroli
2007	J	`jnl`	User Interaction with the Matita Proof Assistant. J. Autom. Reason. Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2007	—	`conf`	Working with Mathematical Structures in Type Theory. TYPES Claudio Sacerdoti Coen, Enrico Tassi
2006	—	`conf`	A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus. MKM Serge Autexier, Claudio Sacerdoti Coen
2006	—	`conf`	Crafting a Proof Assistant. TYPES Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2006	—	`conf`	Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I. WRS@FLoC Claudio Sacerdoti Coen
2006	—	`conf`	Tinycals: Step by Step Tacticals. UITP@FLoC Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2005	—	`conf`	An Interactive Algebra Course with Formalised Proofs and Definitions. MKM Andrea Asperti, Herman Geuvers, Iris Loeb, Lionel Elie Mamane, Claudio Sacerdoti Coen
2005	—	`conf`	Explanation in Natural Language of lamda-µµ-Terms. MKM Claudio Sacerdoti Coen
2004	—	`conf`	A Content Based Mathematical Search Engine: Whelp. TYPES Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli
2004	B	`conf`	A Generative Approach to the Implementation of Language Bindings for the Document Object Model. GPCE Luca Padovani, Claudio Sacerdoti Coen, Stefano Zacchiroli
2004	—	`conf`	A Semi-reflexive Tactic for (Sub-)Equational Reasoning. TYPES Claudio Sacerdoti Coen
2004	—	`conf`	Efficient Ambiguous Parsing of Mathematical Formulae. MKM Claudio Sacerdoti Coen, Stefano Zacchiroli
2004	—	`—`	Knowledge management of formal mathematics and interactive theorem proving. Claudio Sacerdoti Coen
2004	—	`conf`	Mathematical Libraries as Proof Assistant Environments. MKM Claudio Sacerdoti Coen
2004	A*	`conf`	Schemapath, a minimal extension to xml schema for conditional constraints. WWW Claudio Sacerdoti Coen, Paolo Marinelli, Fabio Vitali
2003	—	`conf`	A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics. ICTCS Claudio Sacerdoti Coen
2003	—	`conf`	From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. MKM Claudio Sacerdoti Coen
2003	J	`jnl`	Mathematical Knowledge Management in HELM. Ann. Math. Artif. Intell. Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Ferruccio Guidi, Irene Schena
2001	—	`conf`	HELM and the Semantic Math-Web. TPHOLs Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena
2001	—	`conf`	XML, Stylesheets and the Re-mathematization of Formal Content. Extreme Markup Languages® Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena