Claudio Sacerdoti Coen

Dataset, November, 2024

Reversible debugging of concurrent Erlang programs: Supporting imperative primitives.

[BibT_eX]

[DOI]

Pietro Lami

Ivan Lanese

Jean-Bernard Stefani

Giovanni Fabbretti

J. Log. Algebraic Methods Program., 2024

IMELL Cut Elimination with Linear Overhead.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

2023

Causal Reversibility Implies Time Reversibility.

[BibT_eX]

[DOI]

Marco Bernardo

Ivan Lanese

Andrea Marin

Claudio Antares Mezzina

Sabina Rossi

Proceedings of the Quantitative Evaluation of Systems - 20th International Conference, 2023

Formalizing Functions as Processes.

[BibT_eX]

[DOI]

Horace Blanc

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

Properties of a Computational Lambda Calculus for Higher-Order Relational Queries.

[BibT_eX]

[DOI]

Riccardo Treglia

Proceedings of the 24th Italian Conference on Theoretical Computer Science, 2023

2022

Reversibility in Erlang: Imperative Constructs.

[BibT_eX]

[DOI]

Pietro Lami

Ivan Lanese

Jean-Bernard Stefani

Giovanni Fabbretti

Proceedings of the Reversible Computation - 14th International Conference, 2022

2021

Strong Call-by-Value is Reasonable, Implosively.

[BibT_eX]

[DOI]

Andrea Condoluci

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2020

Pre-Proceedings of the 28th International Workshop on Functional and Logic Programming (WFLP 2020).

[BibT_eX]

[DOI]

Michael Hanus

CoRR, 2020

Logic-Independent Proof Search in Logical Frameworks - (Short Paper).

[BibT_eX]

[DOI]

Michael Kohlhase

Florian Rabe

Jan Frederik Schaefer

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Implementing type theory in higher order constraint logic programming.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2019

Sharing Equality is Linear.

[BibT_eX]

[DOI]

Andrea Condoluci

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

Crumbling Abstract Machines.

[BibT_eX]

[DOI]

Andrea Condoluci

Giulio Guerrieri

Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019

Relational Data Across Mathematical Libraries.

[BibT_eX]

[DOI]

Makarius Wenzel

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

A Plugin to Export Coq Libraries to XML.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

The Coq Library as a Theory Graph.

[BibT_eX]

[DOI]

Dennis Müller

Florian Rabe

Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

On the Prediction of Smart Contracts' Behaviours.

[BibT_eX]

[DOI]

Cosimo Laneve

Adele Veschetti

Proceedings of the From Software Engineering to Formal Methods and Tools, and Back, 2019

2018

Towards an Implementation in LambdaProlog of the Two Level Minimalist Foundation (short paper).

[BibT_eX]

[DOI]

Alberto Fiori

Proceedings of the Joint Proceedings of the CME-EI, 2018

2017

On the value of variables.

[BibT_eX]

[DOI]

Inf. Comput., 2017

2016

A Survey on Retrieval of Mathematical Knowledge.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2016

Implementing HOL in an Higher Order Logic Programming Language.

[BibT_eX]

[DOI]

Cvetan Dunchev

Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2016

2015

ELPI: Fast, Embeddable, λProlog Interpreter.

[BibT_eX]

[DOI]

Cvetan Dunchev

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

On the Relative Usefulness of Fireballs.

[BibT_eX]

[DOI]

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014

Matita Tutorial.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2014

On the Correctness of a Branch Displacement Algorithm.

[BibT_eX]

[DOI]

Jaap Boender

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

2013

Certified Complexity (CerCo).

[BibT_eX]

[DOI]

Ian Stark

Paolo Tranquilli

Proceedings of the Foundational and Practical Aspects of Resource Analysis, 2013

2012

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.

[BibT_eX]

[DOI]

J. Autom. Reason., 2012

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2012

Lebesgue's dominated convergence theorem in Bishop's style.

[BibT_eX]

[DOI]

Enrico Zoli

Ann. Pure Appl. Log., 2012

A Term Rewriting System for Kuratowski's Closure-Complement Problem.

[BibT_eX]

[DOI]

Osama Al-Hassani

Quratul-ain Mahesar

Volker Sorge

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.

[BibT_eX]

[DOI]

Dominic P. Mulligan

Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011

Certified Complexity.

[BibT_eX]

[DOI]

Ian Stark

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

Formalising Overlap Algebras in Matita.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2011

A Foundational View on Integration Problems.

[BibT_eX]

[DOI]

Florian Rabe

Michael Kohlhase

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.

[BibT_eX]

[DOI]

Maria Emilia Maietti

Giovanni Sambin

Silvio Valentini

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

The Matita Interactive Theorem Prover.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

Declarative Representation of Proof Terms.

[BibT_eX]

[DOI]

J. Autom. Reason., 2010

Preface.

[BibT_eX]

[DOI]

David Aspinall

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

General Recursion and Formal Topology

[BibT_eX]

[DOI]

Silvio Valentini

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

Regular Expressions, au point

[BibT_eX]

[DOI]

CoRR, 2010

Functions as Processes: Termination and the lm[(m)\tilde]\lambda\mu\widetilde{\mu}-Calculus.

[BibT_eX]

[DOI]

Matteo Cimini

Davide Sangiorgi

Proceedings of the Trustworthly Global Computing - 5th International Symposium, 2010

Some Considerations on the Usability of Interactive Provers.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Nonuniform Coercions via Unification Hints

[BibT_eX]

[DOI]

Proceedings of the Proceedings Types for Proofs and Programs, Revised Selected Papers, 2009

Hints in Unification.

[BibT_eX]

[DOI]

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

Natural Deduction Environment for Matita.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics, 2009

2008

Spurious Disambiguation Errors and How to Get Rid of Them.

[BibT_eX]

[DOI]

Math. Comput. Sci., 2008

A constructive and formal proof of Lebesgue's Dominated Convergence Theorem in the interactive theorem prover Matita.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2008

A User Interface for a Mathematical System that Allows Ambiguous Formulae.

[BibT_eX]

[DOI]

Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2008

2007

User Interaction with the Matita Proof Assistant.

[BibT_eX]

[DOI]

J. Autom. Reason., 2007

Working with Mathematical Structures in Type Theory.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Conference, 2007

Spurious Disambiguation Error Detection.

[BibT_eX]

[DOI]

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

Tinycals: Step by Step Tacticals.

[BibT_eX]

[DOI]

Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, 2006

Reduction and Conversion Strategies for the Calculus of (co)Inductive Constructions: Part I.

[BibT_eX]

[DOI]

Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming, 2006

Crafting a Proof Assistant.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2006

A Formal Correspondence Between OMDoc with Alternative Proofs and the lambdaµµ-Calculus.

[BibT_eX]

[DOI]

Serge Autexier

Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

2005

Explanation in Natural Language of lamda-µµ-Terms.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

An Interactive Algebra Course with Formalised Proofs and Definitions.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004

Knowledge management of formal mathematics and interactive theorem proving.

[BibT_eX]

[DOI]

PhD thesis, 2004

Schemapath, a minimal extension to xml schema for conditional constraints.

[BibT_eX]

[DOI]

Paolo Marinelli

Fabio Vitali

Proceedings of the 13th international conference on World Wide Web, 2004

A Semi-reflexive Tactic for (Sub-)Equational Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

A Content Based Mathematical Search Engine: Whelp.

[BibT_eX]

[DOI]

Proceedings of the Types for Proofs and Programs, International Workshop, 2004

Efficient Ambiguous Parsing of Mathematical Formulae.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

Mathematical Libraries as Proof Assistant Environments.

[BibT_eX]

[DOI]

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

A Generative Approach to the Implementation of Language Bindings for the Document Object Model.

[BibT_eX]

[DOI]

Proceedings of the Generative Programming and Component Engineering: Third International Conference, 2004

2003

Mathematical Knowledge Management in HELM.

[BibT_eX]

[DOI]

Irene Schena

Ann. Math. Artif. Intell., 2003

From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Computer Science, 8th Italian Conference, 2003

2001

HELM and the Semantic Math-Web.

[BibT_eX]

[DOI]

Irene Schena

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

XML, Stylesheets and the Re-mathematization of Formal Content.

[BibT_eX]

[DOI]