Claudio Sacerdoti Coen

According to our database1, Claudio Sacerdoti Coen authored at least 54 papers between 2001 and 2019.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Relational Data Across Mathematical Libraries.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

A Plugin to Export Coq Libraries to XML.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

The Coq Library as a Theory Graph.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

2018
Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper).
Proceedings of the Joint Proceedings of the CME-EI, 2018

2016
Implementing HOL in an Higher Order Logic Programming Language.
Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2016

2015
A Survey on Retrieval of Mathematical Knowledge.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

ELPI: Fast, Embeddable, \lambda Prolog Interpreter.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

On the Relative Usefulness of Fireballs.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014
Matita Tutorial.
J. Formalized Reasoning, 2014

On the Value of Variables.
Proceedings of the Logic, Language, Information, and Computation, 2014

On the Correctness of a Branch Displacement Algorithm.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

2013

2012
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.
J. Autom. Reasoning, 2012

Preface.
Electr. Notes Theor. Comput. Sci., 2012

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
Logical Methods in Computer Science, 2012

Lebesgue's dominated convergence theorem in Bishop's style.
Ann. Pure Appl. Logic, 2012

A Term Rewriting System for Kuratowski's Closure-Complement Problem.
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.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

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

Formalising Overlap Algebras in Matita.
Mathematical Structures in Computer Science, 2011

A Foundational View on Integration Problems.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

The Matita Interactive Theorem Prover.
Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010
Declarative Representation of Proof Terms.
J. Autom. Reasoning, 2010

General Recursion and Formal Topology
Proceedings of the Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010

Functions as Processes: Termination and the lm[(m)\tilde]\lambda\mu\widetilde{\mu}-Calculus.
Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

General Recursion and Formal Topology.
Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010

Some Considerations on the Usability of Interactive Provers.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009
A User Interface for a Mathematical System that Allows Ambiguous Formulae.
Electr. Notes Theor. Comput. Sci., 2009

Nonuniform Coercions via Unification Hints
Proceedings of the Proceedings Types for Proofs and Programs, Revised Selected Papers, 2009

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

Natural Deduction Environment for Matita.
Proceedings of the Intelligent Computer Mathematics, 2009

2008
Spurious Disambiguation Errors and How to Get Rid of Them.
Mathematics in Computer Science, 2008

A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita.
J. Formalized Reasoning, 2008

2007
User Interaction with the Matita Proof Assistant.
J. Autom. Reasoning, 2007

Tinycals: Step by Step Tacticals.
Electr. Notes Theor. Comput. Sci., 2007

Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I.
Electr. Notes Theor. Comput. Sci., 2007

Working with Mathematical Structures in Type Theory.
Proceedings of the Types for Proofs and Programs, International Conference, 2007

Spurious Disambiguation Error Detection.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006
Crafting a Proof Assistant.
Proceedings of the Types for Proofs and Programs, International Workshop, 2006

A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus.
Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

2005
Explanation in Natural Language of lamda-µµ-Terms.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

An Interactive Algebra Course with Formalised Proofs and Definitions.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004
Schemapath, a minimal extension to xml schema for conditional constraints.
Proceedings of the 13th international conference on World Wide Web, 2004

A Semi-reflexive Tactic for (Sub-)Equational Reasoning.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

A Content Based Mathematical Search Engine: Whelp.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Efficient Ambiguous Parsing of Mathematical Formulae.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

Mathematical Libraries as Proof Assistant Environments.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

A Generative Approach to the Implementation of Language Bindings for the Document Object Model.
Proceedings of the Generative Programming and Component Engineering: Third International Conference, 2004

2003
Mathematical Knowledge Management in HELM.
Ann. Math. Artif. Intell., 2003

From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls.
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.
Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2001
HELM and the Semantic Math-Web.
Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

XML, Stylesheets and the Re-mathematization of Formal Content.
Proceedings of the Extreme Markup Languages® 2001 Conference, 2001


  Loading...