Logo of the University of Bologna
About myself
Short curriculum vitae
Research topics
Current work
Previous work
Publications
Presentations
MoWGLI reports
Interesting links
Teaching duties
Tutorials
Valid XHTML 1.0! Valid CSS!

Last update: 29/09/2009

Claudio Sacerdoti Coen (aka CSC)

 

Name:   Claudio
Surname:   Sacerdoti Coen
Birth place and date:   Bologna (IT), 12/07/1976
 
Qualification:   Ph.D. Doctor in Computer Science
Employment:   Lecturer in Computer Science
Affiliation:   Department of Computer Science,
University of Bologna
 
Office:   via Mura Anteo Zamboni n. 7, 40126, Bologna (IT)
Telephone number:   +39 051 2094973
Fax number:   +39 051 2094510 / +39 051 2094983
 
Home:   via Treviso n. 1, 40139, Bologna (IT)
 
E-Mail:   sacerdot@cs.unibo.it
  Me with a cheetah

Short curriculum vitae

I got my diploma the 25 of July 1995 (rating 60/60), after attending a school where I was taught in particular mathematics, physics and chemistry.

I attended the course in Computer Science, specialisation in Software Systems, of the faculty of Mathematical, Physical and Natural Science of the University of Bologna, that I finished the 12th of October 2000 with rating 110/110 cum laude. The title of my Master Thesis (that gave me a title equivalent to baccalaureate + 5) was "Progettazione e realizzazione con tecnologia XML di basi distribuite di conoscenza matematica formalizzata" ("Design and implementation using XML tecnology of distributed libraries of formalized mathematical knowledge"). During the last four years of university I was also a system administrator of a Linux host of my department, thanks to the Caristudenti project.

From the 14th of October 2000 to the end of December 2000 I was guest of project Logical at the Rocquencourt Research Unit of INRIA (Institute National de Recherche en Informatique et Automatique). Next, from the 8th of January 2001 to the 24th of February 2001, I worked as a Scientific Consultant for project Formavie at the Sophia-Antipolis Research Unit of INRIA.

From the 27th February 2001 to the 21st April 2004 I have been a student of the Dottorato di Ricerca in Informatica (Italian equivalent of a PhD. Student position) at the Department of Computer Science of the University of Bologna.

The 21st April 2004 I successfully defended my PhD. thesis, whose title is "Knowledge Management of Formal Mathematics and Interactive Theorem Proving".

After my PhD. and until the 30th June 2004 I had a temporary position as a research assistant at the Department of Computer Science, University of Bologna

From the 1st July 2004 to the 31 May 2005 I have been a Post-Doc at INRIA (Institute National de Recherche en Informatique et Automatique), in the Logical research team.

From the 6th June 2005 I am a lecturer at the Department of Computer Science, University of Bologna.

Research topics

My principal line of research is the study of the integration of XML-based Mathematical Knowledge Management technologies with Interactive Theorem Proving.

More generally, I am interested in:

Current work

I am leader of project DAMA (Dimostrazione Assistita per la Matematica e l'Apprendimento) that studies the application of interactive theorem proving techniques to didactics of mathematics.

My most time consuming research activity consists in the development of the interactive theorem prover Matita, that is at the core of project DAMA.

Matita is based on the Calculus of (co)Inductive Constructions and tightly integrates several concepts and tools from the domain of Mathematical Knowledge Management.

It is also characterized by its code base kept as simple as possible, without sacrifying well assessed features (extensible notation, coercions, refinement) as well as innovative ones (ambiguous notation, complex search, MathML based natural language rendering).

Previous work

I used to lead the "Transformations" work-package of the IST European Project MOWGLI (Math on the Web: Get it by Logic and Interfaces) that is meant to provide XML-based technologies for publishing, distributing, rendering and searching mathematical documents on the Web.

Project MoWGLI capitalises over the experience of several previous projects, one of them being HELM (Hypertextual Electronic Library of Mathematics) that is a long term projects of the University of Bologna focused on formal mathematical knowledge. I have been one of the principal developers of HELM since its beginning in 1999.

HELM is focused on the integration of the current tools for the automation of formal reasoning and the mechanisation of mathematics (proof assistants and logical frameworks) with the most recent technologies for the development of web applications and electronic publishing, eventually passing through the Extensible Markup Language. The final aim is the development of a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge.

In particular, inside both HELM and MoWGLI, I worked on

  1. exporting from Coq to XML the definitions and theorems written in the Calculus of (Co)Inductive Constructions
  2. the development of a proof-checker and a proof assistant for those theorems
  3. the implementation of a browser able to interface to the proof-checker and able to "annotate" them to make them understandable.

using the following W3C standards

XML
To encode the mathematical theories
MathML
To render the mathematical theories
XSLT
To translate the encoded theories to MathML content markup and to translate content markup to presentation markup
XLINK
To get back from presentation to content markup and from MathML to XML
RDF
To add metadata to the mathematical theories

Publications

In each category the publications are in reverse chronological order.

Theses

  1. C. Sacerdoti Coen.
    Mathematical Knowledge Management and Interactive Theorem Proving.
    PhD. thesis, Department of Computer Science, University of Bologna.

  2. C. Sacerdoti Coen.
    Progettazione e realizzazione con tecnologia XML di basi distribuite di conoscenza matematica formalizzata.
    Master thesis (Italian version only).
    Also available as [HTML version] e [HTML version (single page)]
    Abstract: Fully describes the status of project HELM and the design and implementation choises taken from its birth to autumn 2000.

International Journals

  1. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E. Tassi
    Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.
    To appear in Journal of Formal Reasoning, 1-25, ISSN:0168-7433, 2012.
    Abstract:

  2. C.Sacerdoti Coen, E. Zoli
    Lebesgue's dominated convergence theorem in Bishop's style.
    In Annals of Pure and Applied Logic, 163(2): 140-150, 2012.
    Abstract:

  3. C.Sacerdoti Coen, E. Tassi
    Formalizing Overlap Algebras in Matita.
    In Mathematical Structures in Computer Science 21(4): 763-793 (2011).
    Abstract:

  4. C.Sacerdoti Coen.
    Declarative Representation of Proof Terms.
    In Special Issue on Programming Languages for Mechanized Mathematical Systems, Journal of Automated Reasoning, Carrette, Wenzel and Wiedijk editors, to appear in 2009. A shorter version was published in Programming Languages for Mechanized Mathematics Workshop, RISC Report Series, University of Linz (Austria), vol. 07-10, Pages 3-18, July 2007.
    Abstract: We present a declarative language inspired by the pseudo-natural language previously used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.

  5. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi.
    A compact kernel for the calculus of inductive constructions.
    In Special Issue on Iteractive Proving and Proof Checking of the Academy Journal of Engineering Sciences (Sadhana) of the Indian Academy of Sciences. SADHANA (BANGALORE). vol. 34(1), pp. 71 - 144 ISSN: 0256-2499, 2009
    Abstract: The paper describes the new kernel for the Calculus of Inductive Construc-tions (CIC) implemented inside the Matita Interactive Theorem Prover. The design of the new kernel has been completely revisited since the first release, resulting in a remarkably compact implementation of about 2300 lines of OCaml code. The work is meant for people interested in implementation aspects of Interactive Provers, and is not self contained. In particular, it requires good acquaintance with Type Theory and functional programming languages.

  6. C.Sacerdoti Coen, E.Tassi.
    A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita.
    Journal of Formalized Reasoning. vol. 1, pp. 51 - 89, 2008, ISSN: 1972-5787.
    Abstract: We present a formalisation of a constructive proof of Lebesgue’s Dominated Convergence Theorem given by the Sacerdoti Coen and Zoli in [CSCZ]. The proof is done in the abstract setting of ordered uniformities, also introduced by the two authors as a simplification of Weber’s lattice uniformities given in [Web91, Web93]. The proof is fully constructive, in the sense that it is done in Bishop’s style and, under certain assumptions, it is also fully predicative. The formalisation is done in the Calculus of (Co)Inductive Constructions using the interactive theorem prover Matita [ASTZ07]. It exploits some peculiar features of Matita and an advanced technique to represent algebraic hierarchies previously introduced by the authors in [ST07]. Moreover, we introduce a new technique to cope with duality to halve the formalisation effort.

  7. C.Sacerdoti Coen, S.Zacchiroli.
    Spurious Disambiguation Errors and How to Get Rid of Them.
    Journal of Mathematics in Computer Science, special issue on Management of Mathematical Knowledge, vol. 2, pp. 355 - 378, 2008, ISSN 1661-8270, Birkhäuser/Springer.
    Abstract: The disambiguation approach to the input of formulae enables users of mathematical assistants to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae however, far too many typing errors are generated; among them we want to present only errors related to the formula interpretation meant by the user, hiding errors related to other interpretations.
    We study disambiguation errors and how to classify them into the spurious and genuine error classes. To this end we give a general presentation of the classes of disambiguation algorithms and efficient disambiguation algorithms. We also quantitatively assess the quality of the presented error classification criteria benchmarking them in the setting of a formal development of constructive algebra.

  8. A.Asperti, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli.
    User Interaction with the Matita Proof Assistant.
    In Journal of Automated Reasoning, Kluwer Academic Publishers, 39(2): 109--139, ISSN:0168-7433 2007.
    Abstract: Matita is a new, document-centric, tactic-based interactive theorem prover. This paper focuses on some of the distinctive features of the user interaction with Matita, mostly characterized by the organization of the library as a searchable knowledge base, the emphasis on a high-quality notational rendering, and the complex interplay between syntax, presentation, and semantics.

  9. A.Asperti, F.Guidi, L.Padovani, C.Sacerdoti Coen, I.Schena.
    Mathematical Knowledge Management in HELM.
    In Annals of Mathematics and Artificial Intelligence, 38(1): 27--46; Maggio 2003. A previous version was published in On-Line Proceedings of the First International Workshop on Mathematical Knowledge Management ( MKM2001), RISC-Linz, Austria, September 2001.
    Abstract: The paper describes the general philosophy and the main architectural and technological solutions of the HELM Project for the management of large repositories of mathematical knowledge. The lait-motif is the extensive use of XML-technology, and the exploitation of information in the "Web way", that is without central authority, with few basic rules, in a scalable, adaptable, and extensible manner.

Acts of International Conferences

  1. R. Armadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. Regis-Gianas, C. Sacerdoti Coen, I. Stark
    Certified Complexity.
    In PROCEDIA COMPUTER SCIENCE. 2nd European Future Technologies Conference and Exhibition 2011 (FET 11). Budapest. 4-6/05/2011. vol. 7, pp. 175 - 177 ISSN: 1877-0509, 2011
    Abstract:

  2. F.Rabe, M.Kohlhase, C.Sacerdoti Coen
    A Foundational View on Integration Problems.
    In Intelligent Computer Mathematics, Proceedings of the 18th Symposium Calculemus and 10th international conference Mathematical Knowledge Management, Lecture Notes in Artificial Intelligence, ISBN:978-3-642-22672-4, 6824, 107-122, 2011.
    Abstract:

  3. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi
    The Matita Interactive Theorem Prover.
    In Automated Deduction – CADE-23, LECTURE NOTES IN COMPUTER SCIENCE, ISBN:978-3-642-22437-9, Pages 64-69, Volume 6803, Year 2011 64-69.
    Abstract:

  4. A.Asperti, M.E.Maietti, C.Sacerdoti Coen, G.Sambin, S.Valentini
    Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita.
    In Proceedings of Calculemus/MKM 2011, Lecture Notes in Artificial Intelligence, 6824, Pages 278-280, 2011.
    Abstract:

  5. A.Asperti, C.Sacerdoti Coen
    Some Considerations on the Usability of Interactive Provers.
    In Intelligent Computer Mathematics, Lecture Notes in Computer Science, ISBN:978-3-642-14127-0, 6167, Pages 147-156, 2010.
    Abstract:

  6. C.Sacerdoti Coen, S. Valentini
    General Recursion and Formal Topology.
    In Proceedings of PAR 2010, Electronic Proceedings in Theoretical Computer Science, ISSN:20752180, 43, Pages 65-75
    Abstract:

  7. M.Cimini, D.Sangiorni, C.Sacerdoti Coen
    Functions as Processes: Termination and the λµµ-Calculus.
    In Trustworthly Global Computing, Lecture Notes in Computer Science, ISBN:978-3-642-15639-7, 6084, Pages 73-86, 2010.
    Abstract:

  8. C. Sacerdoti Coen, E. Tassi
    Nonuniform Coercions via Unification Hints In Proceedings Types for Proofs and Programs, Revised Selected Papers, ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE (EPTCS), ISSN:2075-2180, DOI:10.4204/EPTCS.53.2, vol. 53, 19-26, March 2011.
    Abstract: We introduce the notion of nonuniform coercion, which is the promotion of a value of one type to an enriched value of a different type via a nonuniform procedure. Nonuniform coercions are a generalization of the (uniform) coercions known in the literature and they arise naturally when formalizing mathematics in an higher order interactive theorem prover using convenient devices like canonical structures, type classes or unification hints. We also show how nonuniform coercions can be naturally implemented at the user level in an interactive theorem prover that allows unification hints.
  9. A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi
    A New Type for Tactics.
    In proceedings of ACM SIGSAM PLMMS 09, ISBN 978-1-60558-735-6, Pages 27-50, 2009.
    Abstract:

  10. C. Sacerdoti Coen, E. Tassi
    Natural Deduction Environment for Matita In Intelligent Computer Mathematics, CICM 2009, July 2009. LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, ISSN: 0302-9743, vol. 5625. 486-491.
    Abstract: Matita is a proof assistant characterised by a rich, user extensible, output facility based on a widget for the rendering of MathML Presentation, and by the automatic handling of overloading by means of a flexible disambiguation mechanism. We show how to use these features to obtain a simple learning environment for natural deduction, without modifying the source code or Matita.
  11. A. Asperti, W. Ricciotti, C. Sacerdoti Coen, E. Tassi
    Hints in Unification In Proceedings of Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, August 17-20, 2009. LECTURE NOTES IN COMPUTER SCIENCE, ISBN:978-3-642-03358-2, vol. 5674. 84-98.
    Abstract: Several mechanisms such as Canonical Structures, Type Classes, or Pullbacks have been recently introduced with the aim to improve the power and flexibility of the type inference algorithm for interactive theorem provers. We claim that all these mechanisms are particular instances of a simpler and more general technique, just consisting in providing suitable hints to the unification procedure underlying type inference. This allows a simple, modular and not intrusive implementation of all the above mentioned techniques, opening at the same time innovative and unexpected perspectives on its possible applications.
  12. C. Sacerdoti Coen
    A User Interface for a Mathematical Systems that Allows Ambiguous Formulae In Proceedings of 8th International Workshop On User Interfaces for Theorem Provers. Montréal, Québec, Canada, 22nd August 2008, ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, ISSN: 1571-0661, vol. 226, pp. 67-87.
    Abstract: Mathematical systems that understand the usual ambiguous mathematical notation need well thought out user interfaces 1) to provide feedback on the way formulae are automatically interpreted, when a single best interpretation exists; 2) to dialogue with the user when human intervention is required because multiple best interpretations exist; 3) to present sets of errors to the user when no correct interpretation exists. In this paper we discuss how we handle ambiguity in the user interfaces of the Matita interactive theorem prover and the Whelp search engine.
  13. C. Sacerdoti Coen, E. Zoli
    Lebesgue's Dominated Convergence Theorem in Bishop's Style Technical Report of the University of Bologna (Italy), Department of Computer Science, UBLCS-2008-18. Submitted to Annals of Pure and Applied Logic, Special Issue on 3rd Workshop on Formal Topology.
    Abstract: We present a constructive proof in Bishop's style of Lebesgue's dominated convergence theorem in the abstract setting of ordered uniform spaces. The proof generalises to this setting a classical proof in the framework of uniform lattices presented by Hans Weber in "Uniform Lattices II: Order Continuity and Exhaustivity", in Annali di Matematica Pura ed Applicata (IV), Vol. CLXV (1993).
  14. C. Sacerdoti Coen, E. Tassi
    Working with Mathematical Structures in Type Theory In Proceedings of TYPES 2007: Conference of the Types Project, 2-5 May 2007 Cividale del Friuli (Udine), Italy. LNCS, ISSN 0302-9743 (Print) 1611-3349 (Online), DOI 10.1007/978-3-540-68103-8, ISBN 978-3-540-68084-0, Pages 157-172, Volume 4941, Year 2008.
    Abstract: We address the problem of representing mathematical structures in a proof assistant which: 1) is based on a type theory with dependent types, telescopes and a computational version of Leibniz equality; 2) implements coercive subtyping, accepting multiple coherent paths between type families; 3) implements a restricted form of higher order unification and type reconstruction. We show how to exploit the previous quite common features to reduce the ``syntactic'' gap between pen&paper and formalised algebra. However, to reach our goal we need to propose unification and type reconstruction heuristics that are slightly different from the ones usually implemented. We have implemented them in Matita.
  15. C. Sacerdoti Coen, E. Zoli
    A Note on Formalizing Undefined Terms in Real Analysis In Herman Geuvers, Pierre Courtieu, proceedings of PATE 07, International Workshop on Proof Assistants and Types in Education, Paris 25/06/2007. Pages 3-16, June 2007.
    Abstract: To adopt proof assistants based on logic of total functions in education, one major problem is that of representing partial functions. In particular, one wishes to capture undefinedness in a rigorous way, while staying as close as possible to traditional mathematical practice. In this paper, we propose to represent potentially undefined terms with partial setoids on lifted terms, and to understand book equalities occurring in equality chains as special directed relations that hold only under assumptions of definedness for some terms. We also employ a suitable notion of strict morphism to fully automate propagation of these directed relations in strict contexts.
  16. C. Sacerdoti Coen
    Declarative Representation of Proof Terms In Programming Languages for Mechanized Mathematics Workshop, RISC Report Series, University of Linz (Austria), vol. 07-10, Pages 3-18, July 2007.
    Abstract: We present a declarative language inspired by the pseudo-natural language used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.
  17. C. Sacerdoti Coen, S. Zacchiroli
    Spurious Disambiguation Error Detection In Towards Mechanized Mathematical Assistants, Lecture Notes in Artificial Intelligence (LNAI), Springer Berlin / Heidelberg, Vol. 4573, ISBN: 978-3-540-73083-5, Pages 381-392, August 2007.
    Abstract: The disambiguation approach to the input of formulae enables the user to type correct formulae in a terse syntax close to the usual ambiguous mathematical notation. When it comes to incorrect formulae we want to present only errors related to the interpretation meant by the user, hiding errors related to other interpretations (spurious errors). We propose a heuristic to recognize spurious errors, which has been integrated with the disambiguation algorithm of "Efficient Ambiguous Parsing of Mathematical Formulae" (Sacerdoti Coen and Zacchiroli, 2004).
  18. C. Sacerdoti Coen
    Reduction and Conversion Strategies for the Calculus of (co)Inductive Construtions: Part I In Proceedings of the Sixth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2006), Elsevier, ENTCS, Volume 174, Issue 10, Pages 97-118, July 2007.
    Abstract: We compare several reduction and conversion strategies for the Calculus of (co)Inductive Constructions by running benchmarks on the library of the Coq proof assistant. All the strategies have been implemented in an independent verifier for the proof objects of Coq that is part of the Matita proof assistant.
  19. A. Asperti, C. Sacerdoti Coen, E. Tassi, S. Zacchiroli
    Crafting a Proof Assistant In Proceedings of Types 2006: Conference of the Types Project. Notthingham, UK, 18-21 April, 2006. Lecture Notes in Computer Science (LNCS), Vol. 4502, ISBN:978-3-540-74463-4, 18--32, 2007.
    Abstract: Proof assistants are complex applications whose development has never been properly systematized or documented. This work is a contribution in this direction, based on our experience with the development of Matita: a new interactive theorem prover based---as Coq---on the Calculus of Inductive Constructions (CIC). In particular, we analyze its architecture focusing on the dependencies of its components, how they implement the main functionalities, and their degree of reusability. The work is a first attempt to provide a ground for a more direct comparison between different systems and to highlight the common functionalities, not only in view of reusability but also to encourage a more systematic comparison of different softwares and architectural solutions.
  20. C. Sacerdoti Coen, E. Tassi, S. Zacchiroli
    Tinycals: Step by Step Tacticals In Proceedings of the 7th Workshop on User Interfaces for Theorem Provers, Elsevier, ENTCS, Volume 174, Issue 2, Pages 125--142, May 2007.
    Abstract: Most of the state-of-the-art proof assistants are based on procedural proof languages, scripts, and rely on LCF tacticals as the primary tool for tactics composition. In this paper we discuss how these ingredients do not interact well with user interfaces based on the same interaction paradigm of Proof General (the de facto standard in this field), identifying in the coarse-grainedness of tactical evaluation the key problem. We propose Tinycals as an alternative to a subset of LCF tacticals, showing that the user does not experience the same problem if tacticals are evaluated in a more fine-grained manner. We present the formal operational semantics of Tinycals as well as their implementation in th Matita proof assistant.
  21. S. Autexier, C.Sacerdoti Coen
    A Formal Correspondence between OMDoc with Alternative Proofs and the lambda-bar-mu-mu-tilde-Calculus In Fifth International Conference on Mathematical Knowledge Management (MKM2006), Lecture Notes in Artificial Intelligence (LNAI), 4108, 67--81, 2006.
    Abstract: We consider an extension of OMDoc proofs with alternative sub-proofs and proofs at different level of detail, and an affine non-deterministic fragment of the lambda-bar-mu-mu-tilde-calculus seen as a proof format. We provide explanations in pseudo-natural language of proofs in both formats, and a formal correspondence between the two by means of two mutually inverse encodings of one format in the other one.
  22. A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen
    An Interactive Algebra Course with Formalised Proofs and Definitions In Fourth International Conference on Mathematical Knowledge Management (MKM2005), Lecture Notes in Artificial Intelligence (LNAI), Vol. 3863, ISBN: 3-540-31430-X, 315--329, 2006.
    Abstract: We describe a case-study of the application of web-technology (HELM) to create Web-based didactic material out of a repository of formal mathematics (CCoRN), using the structure of an existing course (IDA). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the "view"), and the rendering of proofs.
  23. C.Sacerdoti Coen
    Explanation in Natural language of lambda-bar-mu-mu-tilde-terms In Fourth International Conference on Mathematical Knowledge Management (MKM2005), Lecture Notes in Artificial Intelligence (LNAI), Vol. 3863, ISBN: 3-540-31430-X, 234--249, 2006.
    Abstract: The lambda-bar-mu-mu-tilde-calculus, introduced by Curien and Herbelin, is a calculus isomorphic to (a variant of) the classical sequent calculus LK of Gentzen. As a proof format it has very remarkable properties that we plan to study in future works. In this paper we embed it with a rendering semantics that provides explanations in pseudo-natural language of its proof terms, in the spirit of the work of Yann Coscoy for the lambda-calculus. The rendering semantics unveils the richness of the calculus that allows to preserve several proof structures that are identified when encoded in the lambda-calculus.
  24. C.Sacerdoti Coen
    A semi-reflexive tactic for (sub-)equational reasoning In Types for Proofs and Programs International Workshop, TYPES 2004. Lecture Notes in Computer Science (LNCS), Vol. 3839, ISBN: 3-540-31428-8, 99--115, 2006.
    Abstract: We propose a simple theory of monotone functions that is the basis for the implementation of a tactic that generalises one step conditional rewriting by ``propagating'' constraints of the form xRy where the relation R can be weaker than an equivalence relation. The constraints can be propagated only in goals whose conclusion is a syntactic composition of n-ary functions that are monotone in each argument.
    The tactic has been implemented in the Coq system as a semi-reflexive tactic, which represents a novelty and an improvement over an earlier similar development for NuPRL.
    A few interesting applications of the tactic are: reasoning in type theory about equivalence classes (by performing rewriting in well-defined goals); reasoning about reductions and properties preserved by reductions; reasoning about partial functions over equivalence classes (by performing rewriting in PERs); propagating inequalities by replacing a term with a smaller (greater) one in a given monotone context.
  25. A.Asperti, F.Guidi, C.Sacerdoti Coen, E.Tassi, S.Zacchiroli
    A content based mathematical search engine: Whelp In Types for Proofs and Programs International Workshop, TYPES 2004. Lecture Notes in Computer Science (LNCS), Vol. 3839, ISBN: 3-540-31428-8, 17--32, 2006.
    Abstract: The prototype of a content based search engine for mathematical knowledge supporting a small set of queries requiring matching and/or typing operations is described. The prototype --- called Whelp --- exploits a metadata approach for indexing the information that looks far more flexible than traditional indexing techniques for structured expressions like substitution, discrimination, or context trees. The prototype has been instantiated to the standard library of the Coq proof assistant extended with many user contributions.
  26. L.Padovani, C.Sacerdoti Coen, S.Zacchiroli
    A Generative Approach to the Implementation of Language Bindings for the Document Object Model
    In Generative Programming and Component Engineering: Third International Conference, GPCE 2004, Lecture Notes in Computer Science (LNCS), Vol. 3286, ISBN:ISBN 3-540-23580-9, 469--487, 2004.
    Abstract: The availability of a C implementation of the Document Object Model (DOM) offers the interesting opportunity of generating bindings for different programming languages automatically. Because of the DOM bias towards Java-like languages, a C implementation that fakes objects, inheritance, polymorphism, exceptions and uses reference-counting introduces a gap between the API specification and its actual implementation that the bindings should try to close. In this paper we overview the generative approach in this particular context and apply it for the generation of C++ and OCaml bindings.
  27. C.Sacerdoti Coen
    Mathematical Libraries as Proof Assistant Environments
    In Proceedings of the Third International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science (LNCS) 3119, ISBN:3-540-23029-7, 332-346, 2004.
    Abstract: In this paper we analyse the modifications on logical operations --- as proof checking, type inference, reduction and convertibility --- that are required for the identification of a proof assistant environment with a distributed mathematical library, focusing on proof assistants based on the Curry-Howard isomorphism.
    This identification is aimed at the integration of Mathematical Knowledge Management tools with interactive theorem provers: once the distinction between the proof assistant environment and a mathematical library is blurred, it is possible to exploit Mathematical Knowledge Management rendering, indexing and searching services inside an interactive theorem prover, a first step towards effective loosely-coupled collaborative mathematical environments.

  28. C.Sacerdoti Coen, S.Zacchiroli
    Efficient Ambiguous Parsing of Mathematical Formulae
    In Proceedings of the Third International Conference on Mathematical Knowledge Management, Lecture Notes in Computer Science (LNCS) 3119, ISBN:3-540-23029-7, 347-362, 2004.
    Abstract: Mathematical notation has the characteristic of being ambiguous: operators can be overloaded and information that can be deduced is often omitted. Mathematicians are used to this ambiguity and can easily disambiguate a formula making use of the context and of their ability to find the right interpretation.
    Software applications that have to deal with formulae usually avoid these issues by fixing an unambiguous input notation. This solution is annoying for mathematicians because of the resulting tricky syntaxes and becomes a show stopper to the simultaneous adoption of tools characterized by different input languages.
    In this paper we present an efficient algorithm suitable for ambiguous parsing of mathematical formulae. The only requirement of the algorithm is the existence of a "validity" predicate over abstract syntax trees of incomplete formulae with placeholders. This requirement can be easily fulfilled in the applicative area of interactive proof assistants, and in several other areas of Mathematical Knowledge Management.
  29. P.Marinelli, C.Sacerdoti Coen, F.Vitali
    SchemaPath, a Minimal Extension to XML Schema for Conditional Constraints
    In Proceedings of the 13th International World Wide Web Conference, ISBN:1-58113-844-X, ACM Press, New York, NY, USA, 164--174, 2004.
    Abstract: In the past few years, a number of constraint languages for XML documents has been proposed. They are cumulatively called schema languages or validation languages and they comprise, among others, DTD, XML Schema, RELAX NG, Schematron, DSD, xlinkit.
    One major point of discrimination among schema languages is the support of co-constraints, or co-occurrence constraints, e.g., requiring that attribute A is present if and only if attribute B is (or is not) presenting the same element. Although there is no way in XML Schema to express these requirements, they are in fact frequently used in many XML document types, usually only expressed in plain human-readable text, and validated by means of special code modules by the relevant applications.
    In this paper we propose SchemaPath, a light extension of XML Schema to handle conditional constraints on XML documents. Two new constructs have been added to XML Schema: conditions -- based on XPath patterns -- on type assignments for elements and attributes; and a new simple type, xsd:error, for the direct expression of negative constraints (e.g. it is prohibited for attribute A to be present if attribute B is also present).
    A proof-of-concept implementation is provided. A Web interface is publicly accessible for experiments and assessments of the real expressiveness of the proposed extension.

  30. C.Sacerdoti Coen
    A Constructive Proof of the Soundness of the Encoding of Random Access Machines in a Linda Calculus with Ordered Semantics
    In Theoretical Computer Science: 8th Italian Conference, LNCS 2841, pp. 37 -- 57, November 2003.
    Abstract: Random Access Machines (RAMs) are a deterministic Turing-complete formalism especially well suited for being encoded in other formalisms. This is due to the fact that RAMs can be defined starting from very primitive concepts and operations, which are unbounded natural numbers, tuples, successor, predecessor and test for equality to zero. Since these concepts are easily available also in theorem-provers and proof-assistants, RAMs are good candidates for proving Turing-completeness of formalisms using a proof-assistant. In this paper we describe an encoding in Coq of RAMs into a Linda Calculus endowed with the Ordered Semantics. We discuss the main difficulties that must be faced and the techniques we adopted to solve them.

  31. F.Guidi, C.Sacerdoti Coen
    Querying Distributed Digital Libraries of Mathematics
    In Calculemus 2003, Aracne Editrice S.R.L., Therese Hardin e Renaud Rioboo editors, ISBN 88-7999-545-6, pp. 17--30.
    Abstract: Several of the most effective techniques to query libraries of structured mathematics are based on pattern-matching. Among them, there are matching-based queries, unification-based queries and several kinds of queries up to isomorphisms (as associative-commutative rewriting). All of these techniques do not scale when the libraries become large or when they are distributed. In this paper we present a filtering technique that can be applied to locate a set of candidates that are likely to match the given pattern. Thus our technique can be used as a first phase that is followed by the actual matching over the set of candidates. Tests performed over the library of the Coq system (\url{http://coq.inria.fr}) (about 40.000 theorems) show that the candidates can be located rather quickly and that the number of false matches is surprisingly low.

  32. C.Sacerdoti Coen, S.Zacchiroli.
    Brokers and Web-Services for Automatic Deduction: a Case Study
    In Calculemus 2003, Aracne Editrice S.R.L., Therese Hardin e Renaud Rioboo editors, ISBN 88-7999-545-6, pp. 43--57.
    Abstract: We present a planning broker and several Web-Services for automatic deduction. Each Web-Service implements one of the tactics usually available in interactive proof-assistants. When the broker is submitted a "proof status" (an incomplete proof tree and a focus on an open goal) it dispatches the proof to the Web-Services, collects the successful results, and send them back to the client as "hints" as soon as they are available.
    In our experience this architecture turns out to be helpful both for experienced users (who can take benefit of distributing heavy computations) and beginners (who can learn from it).

  33. C.Sacerdoti Coen.
    From Proof-Assistans to Distributed Libraries of Mathematics: Tips and Pitfalls.
    In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer Science, Vol. 2594, pp. 30--44, Springer-Verlag.
    Abstract: When we try to extract to an open format formal mathematical knowledge from libraries of already existing proof-assistants, we must face several problems and make important design decisions. This paper is based on our experiences on the exportation to XML of the theories developed in Coq and NuPRL: we try to collect a set of (hopefully useful) suggestions to pave the way to other teams willing to attempt the same operation.

  34. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
    HELM and the Semantic Math-Web.
    In Proc. of TPHOLS 2001, Springer-Verlag, Lectures Notes in Computer Science (LNCS) Series, 2512.
    Abstract: The eXtensible Markup Language (XML) opens the possibility to start anew, on a solid technological ground, the ambitious goal of developing a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge. In particular, XML provides a central technology for storing, retrieving and processing mathematical documents, comprising sophisticated web-publishing mechanisms (stylesheets) covering notational and stylistic issues. By the application of XML technology to the large repositories of structured, content oriented information offered by Logical Frameworks we meet the ultimate goal of the Semantic Web, that is to allow machines the sharing and exploitation of knowledge in the Web way, i.e. without central authority, with few basic rules, in a scalable, adaptable, extensible manner.

  35. C.Sacerdoti Coen.
    Tactics in Modern Proof-Assistants: the Bad Habit of Overkilling.
    Work in progress presented at TPHOLS 2001. Also in Supplementary Proceedings of the 14th International Conference TPHOLS 2001, pp. 352--367, Edinbugrh, Scotland, UK, September 2001.
    Abstract: In this paper we will remark a common bad habit of tactic implementors in proof-assistants based on the Curry-Howard isomorphism; we name it overkilling. The wide-spreading of overkilling is due to a lack of interest in the term encoding of proofs, that leads to huge, unreadable terms. This contributes to furthermore lowering interest in the terms encoding the proofs and eventually to the concrete impossibility to create effective tools to inspect and process them. After a general presentation of overkilling and its implications, we describe a concrete experience of fixing overkilling in the implementation of a reflexive tactic in system Coq, analyzing the gain with respect to term-size, proof-checking time and term readability.

  36. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
    XML, Stylesheets and the re-mathematization of Formal Content.
    In Electronic Proceedings of EXTREME 2001.
    Abstract: An important part of the descriptive power of mathematics derives from its ability to represent formal concepts in a highly evolved, two-dimensional system of symbolic notations. Tools for the mechanisation of mathematics and the automation of formal reasoning must eventually face the problem of re-mathematization of the logical, symbolic content of the information, especially in view of their integration with the World Wide Web. In a different work, we already discussed the pivotal role that XML technology is likely to play in such an integration. In this paper, we focus on the problem of (Web) publishing, advocating the use of XSL Transformations, in conjunction with MathML, as a standard, application independent and modular way for associating notation to formal mathematical content.

  37. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
    Formal Mathematics on the Web.
    In Proceedings of the Eight International Conference Crimea 2001, Vol. 1, pp. 342-346.
    Abstract: not available

  38. I. Attali, C. Courbis, P. Degenne, A. Fau, J. Fillon, D. Parigot, C. Pasquier, C. Sacerdoti Coen.
    SmartTools: a development environment generator based on XML technologies.
    In XML Technologies and Software Engineering, Toronto, Canada. ICSE'2001, ICSE workshop proceedings.
    Abstract: SmartTools is a development environment generator that provides a structure editor and semantic tools as main features. SmartTools is easy to use thanks to its graphical user interface. Being based on Java and XML technologies offers all the features of SmartTools to any defined language. The main goal of this tool is to provide help and support for designing sofwtare development environments for programming languages as well as domain-specific languages defined with XML technologies.
    Keywords: Java, DOM, XML, BML, XSLT, Program Transformation, Software engineering, Interactive environment.

  39. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
    Formal Mathematics in MathML.   HTML Version   Slides
    Presentation at the MathML International Conference 2000, University of Illinois, Urbana-Champaign, Illinois, USA, October 2000.
    Abstract: not available

  40. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
    Towards a Library of Formal Mathematics.
    In Technical Report of TPHOLS2000 Conference, Portland, Oregon, USA, August 2000.
    Abstract: The eXtensible Markup Language (XML) opens the possibility to start anew, on a solid technological ground, the ambitious goal of developing a suitable technology for the creation and maintenance of a virtual, distributed, hypertextual library of formal mathematical knowledge. In particular, XML provides a central technology for storing, retrieving and processing mathematical documents, comprising sophisticated web-publishing mechanisms (stylesheets) covering notational and stylistic issues. In this paper, we discuss the overall architectural design of the new systems, and our progress in this direction.

  41. A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
    Content-Centric Logical Environments.
    Short Presentation at LICS-2000, Santa Barbara, California, USA, June 2000.
    Abstract: There is a compelling need of integration between the current tools for automation of formal reasoning and mechanization of mathematics (proof assistants and logical frameworks) and the most recent technologies for the development of web applications and electronic publishing. Currently, libraries in logical frameworks are usually saved in two formats: a textual one, in the specific tactical language of the proof assistant, and a compiled (proof checked) one in some internal, concrete representation language. Both representations are obviously unsatisfactory, since they are too oriented to the specific application: the information is not directly available, if not by means of the functionalities offered by the system itself. This is in clear contrast with the main guidelines of the modern Information Society, and its new emphasis on content.

MoWGLI reports

These are a few reports about the MoWGLI European Project that I have co-authored. Most of them are just very short descriptions of the functionalities provided by the corresponding prototype.

  1. A.Asperti, Y.Bertot, H.Geuvers, E.Gimenez, H.Herbelin, P.Libbrecht, L.Padovani, C.Sacerdoti Coen, I.Schena, B.Schutz, C.Weyher.
    Preliminary Report on Application Scenarios and Requirement Analysis
  2. C.Sacerdoti Coen.
    Exportation Module
  3. A.Asperti, M.Kohlhase, C.Sacerdoti Coen.
    Document Type Descriptors
  4. A.Asperti, C.Sacerdoti Coen.
    Stylesheets to Intermediate Representation
  5. A.Asperti, F.Guidi, C.Sacerdoti Coen.
    Tools for automatic extraction of Metadata
  6. C.Sacerdoti Coen.
    Advanced MoWGLI Prototype (distribution)

Presentations

These slides have been presented in a few conferences. Plase, request those that are not listed here.

  1. [mkm05] A set of slides presented at the Fourth International Conference on Mathematical Knowledge Management, Bremen 16th July 2005. They are about a few remarkable properties of the lambda-bar-mu-mu-tilde-calculus as a proof format.

To enjoy the following slides, you need to install ActiveDVI.

  1. [bruxelles.tgz] A set of slides presented at the First MoWGLI Annual Review, Bruxelles, 28th March 2003. They briefly present all the deliverables of the Transformation Working Package which were delivered during the first 12 months of activity of MoWGLI.
  2. [orsay.tgz] Another set of slides presented in two distinct talks at the first Math in Coq Meeting, Orsay, 23rd May 2003. The topic of the first talk was about the MoWGLI machinery to query distributed libraries of formal mathematical results. The second talk was about the HELM and MoWGLI tools to render formal mathematical theorems.

Interesting links

A few links that I find very useful or interesting.

Teaching duties

From the academic year 2012-2013 I am teaching Logic ("Logica per l'informatica"). The teaching material (in Italian only) can be found here.

Constructive mathematics

In the academic year 2010-2011 I am teaching a short course on constructive mathematics to the students of the Collegio d'Eccellenza. The teaching material (in Italian only) can be found here.

Past teaching duties

In the academic years 2008-20011 I used to teach Languages and Strutures ("Linguaggi e Strutture"), which is an introduction to logic and algebra. The teaching material (in Italian only) can be found here.

In the academic years 2005-2006, 2006-2007 and 2007-2008 I used to teach Operating Systems ("Sistemi Operativi [M-Z]") and, in 2007-20008 only, also the associated Laboratory ("Laboratorio di Sistemi Operativi [M-Z]"). All the teachning material related to it (in Italian only) can be found here.

Old teaching material

Introduzione a Linux, al Software Free Source e alla vita in Laboratorio
Slides presented the 1st, 3rd, 7th and 8th October 2002 and the 30th September and 1st, 6th and 7th October 2003. (Italian only).

Tutorials (Italian only)

Come utilizzare CVS sulle Linux (How to use CVS on Linux)
A short tutorial for using CVS on the Linux machines of our lab.