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 

EMail: 

sacerdot@cs.unibo.it 



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 SophiaAntipolis
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 PostDoc
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.
My principal line of research is the study of the integration of
XMLbased Mathematical Knowledge Management technologies with Interactive
Theorem Proving.
More generally, I am interested in:
 Mathematical Knowledge Management
 Interactive Theorem Proving
 Logical frameworks, in particular the Calculus of (Co)Inductive Constructions
 ProofAssistants, in particular Coq
and Matita
 Applications of interactive theorem provers to didactics
(I am currently leading project
DAMA)
 Constructive mathematics
 ProofAssistant interfaces and proof rendering
 Markup languages and related tools, in particular XML, XHTML, MathML, XSLT, XPath
 Functional languages, in particular OCaml
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).
I used to lead the "Transformations" workpackage
of the IST European Project MOWGLI
(Math on the Web:
Get it by Logic and
Interfaces) that is meant to
provide XMLbased 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
 exporting from Coq to XML the definitions and
theorems written in the Calculus of (Co)Inductive
Constructions
 the development of a proofchecker and a proof assistant
for those theorems
 the implementation of a browser able
to interface to the proofchecker 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
In each category the publications are in reverse chronological
order.
Theses
 C. Sacerdoti Coen.
Mathematical Knowledge Management
and Interactive Theorem Proving.
PhD. thesis, Department of Computer Science, University of Bologna.
 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
 A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E. Tassi
A BiDirectional Refinement Algorithm for the Calculus of (Co)Inductive Constructions
In Logical Methods in Computer Science}, 8(1), paper 18, 149, 2012.
Abstract:
 A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E. Tassi
Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover.
In Journal of Automated Reasoning, 49(3): 427451, 2012.
Abstract:
 C.Sacerdoti Coen, E. Zoli
Lebesgue's dominated convergence theorem in Bishop's style.
In Annals of Pure and Applied Logic, 163(2): 140150, 2012.
Abstract:
 R. Armadio, A. Asperti, N. Ayache, B. Campbell, D. Mulligan, R. Pollack, Y. RegisGianas, C. Sacerdoti Coen, I. Stark
Certified Complexity.
In PROCEDIA COMPUTER SCIENCE. 2nd European Future Technologies Conference and Exhibition 2011 (FET 11). Budapest. 46/05/2011. vol. 7, pp. 175  177 ISSN: 18770509, 2011
Abstract:
 C.Sacerdoti Coen, E. Tassi
Formalizing Overlap Algebras in Matita.
In Mathematical Structures in Computer Science 21(4): 763793 (2011).
Abstract:
 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. 0710, Pages 318, July 2007.
Abstract:
We present a declarative language inspired by the pseudonatural 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 regeneration of declarative scripts.
 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: 02562499, 2009
Abstract:
The paper describes the new kernel for the Calculus of Inductive Constructions (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.
 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: 19725787.
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.
 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 16618270, 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.
 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): 109139, ISSN:01687433 2007.
Abstract:
Matita is a new, documentcentric, tacticbased 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
highquality notational rendering, and the complex interplay between
syntax, presentation, and semantics.
 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):
2746; Maggio 2003. A previous version was published
in OnLine Proceedings of the First International
Workshop on Mathematical Knowledge Management (
MKM2001), RISCLinz, 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 laitmotif is the extensive use
of XMLtechnology, 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
 J.Boender, C.Sacerdoti Coen
On the Correctness of a Branch Displacement Algorithm.
In Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014), Lecture Notes in Computer Science Volume 8413, pp 605619, 2014.
Abstract:
 O. AlHassani, Q. Mahesar, C. Sacerdoti Coen, V. Sorge
A Term Rewriting System for Kuratowski's ClosureComplement Problem.
In 23rd International Conference on Rewriting Techniques and Applications (RTA'12)}, LIPICS, ISBN 9783939897385, ISSN 18688969,
Vol. 15, pp. 3852, 2012.
Abstract:
 D.P.Mulligan, C.Sacerdoti Coen
On the Correctness of an Optimising Assembler for the Intel MCS51 Microprocessor.
In Certified Programs and Proofs (CPP2012),
Lecture Notes in Computer Science Volume 7679, 2012, pp 4359, 2012
Abstract:
 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:9783642226724, 6824, 107122, 2011.
Abstract:
 A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi
The Matita Interactive Theorem Prover.
In Automated Deduction – CADE23, LECTURE NOTES IN COMPUTER SCIENCE, ISBN:9783642224379, Pages 6469, Volume 6803, Year 2011 6469.
Abstract:
 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 278280, 2011.
Abstract:
 A.Asperti, C.Sacerdoti Coen
Some Considerations on the Usability of Interactive Provers.
In Intelligent Computer Mathematics, Lecture Notes in Computer Science, ISBN:9783642141270, 6167, Pages 147156, 2010.
Abstract:
 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 6575
Abstract:
 M.Cimini, D.Sangiorni, C.Sacerdoti Coen
Functions as Processes: Termination and the λµµCalculus.
In Trustworthly Global Computing, Lecture Notes in Computer Science, ISBN:9783642156397, 6084, Pages 7386, 2010.
Abstract:
 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:20752180, DOI:10.4204/EPTCS.53.2, vol. 53, 1926, 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.
 A.Asperti, W.Ricciotti, C.Sacerdoti Coen, E.Tassi
A New Type for Tactics.
In proceedings of ACM SIGSAM PLMMS 09, ISBN 9781605587356,
Pages 2750, 2009.
Abstract:
 C. Sacerdoti Coen, E. Tassi
Natural Deduction Environment for Matita
In Intelligent Computer Mathematics, CICM 2009, July 2009. LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, ISSN: 03029743, vol. 5625. 486491.
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.
 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 1720, 2009. LECTURE NOTES IN COMPUTER SCIENCE, ISBN:9783642033582, vol. 5674. 8498.
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.
 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: 15710661, vol. 226, pp. 6787.
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.
 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, UBLCS200818. 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).
 C. Sacerdoti Coen, E. Tassi
Working with Mathematical Structures in Type Theory
In Proceedings of TYPES 2007: Conference of the Types Project, 25 May 2007 Cividale del Friuli (Udine), Italy. LNCS, ISSN 03029743 (Print) 16113349 (Online), DOI 10.1007/9783540681038, ISBN 9783540680840, Pages 157172, 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.
 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 316, 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.
 C. Sacerdoti Coen
Declarative Representation of Proof Terms
In Programming Languages for Mechanized Mathematics Workshop,
RISC Report Series, University of Linz (Austria), vol. 0710,
Pages 318, July 2007.
Abstract:
We present a declarative language inspired by the pseudonatural 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 regeneration of declarative scripts.
 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: 9783540730835, Pages 381392, 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).
 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 97118, 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.
 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, 1821 April, 2006. Lecture Notes in Computer Science
(LNCS), Vol. 4502, ISBN:9783540744634, 1832, 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 basedas Coqon 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.
 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 125142, May 2007.
Abstract:
Most of the stateoftheart 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 coarsegrainedness 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 finegrained manner. We present the formal
operational semantics of Tinycals as well as their implementation in th
Matita proof assistant.
 S. Autexier, C.Sacerdoti Coen
A Formal Correspondence between OMDoc with Alternative Proofs and the lambdabarmumutildeCalculus
In Fifth International Conference on Mathematical Knowledge Management
(MKM2006), Lecture Notes in Artificial Intelligence (LNAI), 4108, 6781, 2006.
Abstract:
We consider an extension of OMDoc proofs with alternative subproofs
and proofs at different level of detail, and an affine
nondeterministic fragment of the lambdabarmumutildecalculus seen as a proof
format. We provide explanations in pseudonatural 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.
 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: 354031430X, 315329, 2006.
Abstract:
We describe a casestudy of the application of webtechnology (HELM) to
create Webbased 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.
 C.Sacerdoti Coen
Explanation in Natural language of lambdabarmumutildeterms
In Fourth International Conference on Mathematical Knowledge Management
(MKM2005), Lecture Notes in Artificial Intelligence (LNAI), Vol. 3863,
ISBN: 354031430X, 234249, 2006.
Abstract:
The lambdabarmumutildecalculus, 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 pseudonatural language
of its proof terms, in the spirit of the work of Yann Coscoy for the
lambdacalculus. The rendering semantics unveils the richness of the
calculus that allows to preserve several proof structures that are
identified when encoded in the lambdacalculus.
 C.Sacerdoti Coen
A semireflexive tactic for (sub)equational reasoning
In Types for Proofs and Programs International Workshop, TYPES 2004.
Lecture Notes in Computer Science (LNCS), Vol. 3839, ISBN: 3540314288,
99115, 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 nary functions that are monotone in each
argument.
The tactic has been implemented in the Coq system as a semireflexive
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 welldefined 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.
 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: 3540314288,
1732, 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.
 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 3540235809, 469487, 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 Javalike languages, a C implementation that fakes objects,
inheritance, polymorphism, exceptions and uses referencecounting
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.
 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:3540230297,
332346, 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
CurryHoward 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 looselycoupled collaborative
mathematical environments.
 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:3540230297,
347362, 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.
 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:158113844X, ACM Press, New York, NY, USA, 164174, 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
coconstraints, or cooccurrence 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 humanreadable 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 proofofconcept implementation is provided. A Web interface is publicly
accessible for experiments and assessments of the real expressiveness of
the proposed extension.
 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 Turingcomplete 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 theoremprovers and proofassistants, RAMs are good
candidates for proving Turingcompleteness of formalisms
using a proofassistant. 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.
 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 8879995456, pp. 1730.
Abstract: Several of the most effective techniques to
query libraries of structured mathematics are based on
patternmatching. Among them, there are matchingbased
queries, unificationbased queries and several kinds of
queries up to isomorphisms (as associativecommutative
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.
 C.Sacerdoti Coen, S.Zacchiroli.
Brokers and
WebServices for Automatic Deduction: a Case Study
In Calculemus 2003, Aracne Editrice S.R.L., Therese Hardin e
Renaud Rioboo editors, ISBN 8879995456, pp. 4357.
Abstract: We present a planning broker and several
WebServices for automatic deduction. Each WebService
implements one of the tactics usually available in
interactive proofassistants. 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 WebServices,
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).
 C.Sacerdoti Coen.
From ProofAssistans to
Distributed Libraries of Mathematics: Tips and
Pitfalls.
In Proc. Mathematical Knowledge Management 2003, Lecture
Notes in Computer Science, Vol. 2594, pp. 3044,
SpringerVerlag.
Abstract: When we try to extract to an open format
formal mathematical knowledge from libraries of already
existing proofassistants, 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.
 A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
HELM and the Semantic
MathWeb.
In Proc. of TPHOLS 2001,
SpringerVerlag, 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 webpublishing 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.
 C.Sacerdoti Coen.
Tactics in Modern
ProofAssistants: the Bad Habit of Overkilling.
Work in progress presented at TPHOLS 2001.
Also in Supplementary Proceedings of the 14th International
Conference TPHOLS 2001,
pp. 352367, Edinbugrh, Scotland, UK, September 2001.
Abstract: In this paper we will remark a common bad
habit of tactic implementors in proofassistants based on the
CurryHoward isomorphism; we name it overkilling. The
widespreading 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 termsize,
proofchecking time and term readability.
 A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
XML, Stylesheets and the
remathematization 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, twodimensional system of
symbolic notations. Tools for the mechanisation of
mathematics and the automation of formal reasoning must
eventually face the problem of remathematization 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.
 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.
342346.
Abstract: not available
 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
domainspecific languages defined with XML
technologies.
Keywords: Java, DOM, XML, BML, XSLT, Program
Transformation, Software engineering, Interactive
environment.
 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,
UrbanaChampaign, Illinois, USA, October 2000.
Abstract: not available
 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 webpublishing 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.
 A.Asperti, L.Padovani, C.Sacerdoti Coen, I.Schena.
ContentCentric Logical
Environments.
Short Presentation at LICS2000,
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.
These are a few reports about the
MoWGLI
European Project that I have coauthored. Most of them
are just very short descriptions of the functionalities provided
by the corresponding prototype.
 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
 C.Sacerdoti Coen.
Exportation Module
 A.Asperti, M.Kohlhase, C.Sacerdoti Coen.
Document Type Descriptors
 A.Asperti, C.Sacerdoti Coen.
Stylesheets to Intermediate Representation
 A.Asperti, F.Guidi, C.Sacerdoti Coen.
Tools for automatic extraction of Metadata
 C.Sacerdoti Coen.
Advanced MoWGLI Prototype (distribution)
These slides have been presented in a few conferences.
Plase, request those that are not listed here.
 [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
lambdabarmumutildecalculus as a proof format.
To enjoy the following slides, you need to install ActiveDVI.
 [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.
 [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.
A few links that I find very useful or interesting.

http://pauillac.inria.fr
"virtual building 8", a community of research groups at
INRIA, Rocquencourt, France, with common interests in
programming language design, semantics, implementation,
proof systems, algorithms, and related topics.

http://coq.inria.fr
The Coq Proof Assistant, written in OCaml and based on the
Calculus of (Co)Inductive Constructions. It also helps in
verifying the correctness of programs written, either in
functional or imperative style, in some variants of ML.

http://caml.inria.fr
The Caml Language: Caml is a stronglytyped functional
programming language from the ML family. Caml Light and
Objective Caml are two implementations of Caml.

http://wwwtcs.inf.tudresden.de/~tews/htmlman3.09
The enhanced ocaml documentation version 3.09. The
enhanced documentation contains the original html version
of the ocaml reference manual with the following
changes:
 Changes (wrt version 3.08) are tagged with icons and
color
 meta symbols of the grammar are "hot" and refer to
their definition
There is also a page containing all grammar rules from
the reference manual for easy and quick reference

http://www.ocamlprogramming.de/programming/downloadcaml.html
This is a repository of useful components, libraries and
tools written in and for OCaml.

http://funlinks.camlcity.org
This is a public board where everybody can announce
software contributions to Objective Caml community.

http://www.w3c.org
The World Wide Web consortium.

http://tecfa.unige.ch/guides/tie/tie.html
A lot of very good minicourses (in French) on HTML, Java,
JS, MySQL, LDAP, MOO, PM, PHP, Soft, TIE, Unix, VRML, XML,
Admin
From the academic year 20122013 I am teaching Logic ("Logica per l'informatica"). The teaching material (in Italian only) can be found
here.
In the academic year 20102011 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 200820011 I used to teach Languages and
Structures ("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 20052006, 20062007 and 20072008 I used to teach
Operating Systems ("Sistemi Operativi [MZ]") and,
in 200720008 only, also the associated Laboratory
("Laboratorio di Sistemi Operativi [MZ]").
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).