Enrico Tassi Homepage / Publications
A language of patterns for subterm selection
with Georges Gonthier.
Published in the proceedings of ITP 2012, LNCS, Volume 7406, Year 2012, Pages 361-376,
DOI: , ISBN: .
Download
See abstract
Abstract:
This paper describes the language of patterns that equips
the SSReflect proof shell extension for the Coq system. Patterns are
used to focus proof commands on subexpressions of the conjecture under
analysis in a declarative manner. They are designed to ease the writing
of proof scripts and to increase their readability and maintainability.
A pattern can identify the subexpression of interest approximating the
subexpression itself, or its enclosing context or both. The user is free to
choose the most convenient option.
Patterns are matched following an extremely precise and predictable
discipline, that is carefully designed to admit an efficient implementation.
In this paper we report on the language of patterns, its matching
algorithm and its usage in the formal library developed by the Mathematical
Components team to support the verification of the Odd Order Theorem.
A bi-directional refinement algorithm for the
Calculus of (Co)Inductive Constructions
with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen.
Published in Logical Methods in Computer Science, volume 8, Pages 1-49, 2012.
DOI:10.2168/LMCS-8(1:18)2012. ISSN: 1860-5974 .
Download
See abstract
Abstract:
The paper describes the refinement algorithm for the Calculus of (Co)Inductive
Constructions (CIC) implemented in the interactive theorem prover Matita. The
refinement algorithm is in charge of giving a meaning to the terms, types and
proof terms directly written by the user or generated by using tactics,
decision procedures or general automation. The terms are written in an
“external syntax” meant to be user friendly that allows omission of
information, untyped binders and a certain liberal use of user defined
sub-typing. The refiner modifies the terms to obtain related well typed terms
in the internal syntax understood by the kernel of the ITP. In particular, it
acts as a type inference algorithm when all the binders are untyped. The
proposed algorithm is bi-directional: given a term in external syntax and a
type expected for the term, it propagates as much typing information as
possible towards the leaves of the term. Traditional mono-directional
algorithms, instead, proceed in a bottom- up way by inferring the type of a
sub-term and comparing (unifying) it with the type expected by its context only
at the end. We propose some novel bi-directional rules for CIC that are
particularly effective. Among the benefits of bi-directionality we have better
error message reporting and better inference of dependent types. Moreover,
thanks to bi-directionality, the coercion system for sub-typing is more
effective and type inference generates simpler unification problems that are
more likely to be solved by the inherently incomplete higher order unification
algorithms implemented. Finally we introduce in the external syntax the notion
of vector of placeholders that enables to omit at once an arbitrary number of
arguments. Vectors of placeholders allow a trivial implementation of implicit
arguments and greatly simplify the implementation of primitive and simple
tactics.
The Matita Interactive Theorem Prover
with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen.
Published in the proceedings of CADE 2011, LNCS 6803, 2011, Pages 64-69,
ISBN 978-3-642-22437-9.
Download
See abstract
Abstract:
Matita is an interactive theorem prover being developed by
the Helm team at the University of Bologna. Its stable version 0.5.x may
be downloaded at http://matita.cs.unibo.it. The tool originated in
the European project MoWGLI as a set of XML-based tools aimed to
provide a mathematician-friendly web-interface to repositories of formal
mathematical knoweldge, supporting advanced content-based function-
alities for querying, searching and browsing the library. It has since then
evolved into a light but fully fledged ITP, particularly suited for the as-
sessment of innovative ideas, both at foundational and logical level. In
this paper, we give an account of the whole system, its peculiarities and
its main applications.
Formal Metatheory of Programming Languages in the
Matita Interactive Theorem Prover
with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen.
Published in the journal of Automated Rasoning, Special Issue on the Poplmark Challenge, Pages 1-25, Year 2011. ISSN: 0168-7433. DOI: 10.1007/s10817-011-9228-z
Download
See abstract
Abstract: This paper is a report about the use of Matita, an
interactive theorem prover under development at the University of Bologna, for
the solution of the POPLmark Challenge, part 1a. We provide three different
formalizations, including two direct solutions using pure de Bruijn and locally
nameless encodings of bound variables, and a formalization using named
variables, obtained by means of a sound translation to the locally nameless
encoding. According to this experience, we also discuss some of the proof
principles used in our solutions, which have led to the development of a
generalized inversion tactic for Matita.
Pointed Regular Expressions
with Andrea Asperti and Claudio Sacerdoti Coen.
Submitted to the LATA2011 conference.
Download
See abstract
Abstract: We introduce a new technique for constructing a finite state
deterministic automaton from a regular expression, based on the idea
of marking a suitable set of positions inside the expression, intuitively
representing the possible points reached after the processing of an ini-
tial prefix of the input string. Pointed regular expressions provide an
algebraic counterpart to position automata, joining the elegance and the
symbolic appealingness of Brzozowski’s derivatives, with the effective-
ness of McNaughton and Yamada’s labelling technique, and essentially
combining the best of the two approaches.
Formalizing Overlap Algebras in Matita
with Claudio Sacerdoti Coen. Journal
Mathematical Structures in Computer Science, Volume 21, Issue 3,
Pages 1-31, Year 2011. ISSN: 0960-1295. EISSN: 1469-8072.
DOI: 10.1017/S0960129511000107.
Download
See abstract
Abstract: We describe the formalization in Matita version ½ of
some results in formal topology presented in predicative intuitionistic logic
and in terms of Overlap Algebras. These are new algebraic structures designed
to reason about subsets in an algebraic way and within intuitionistic logic. As
it turns out, they also ease the formalization of formal topology results in an
interactive theorem prover. The main result presented is the existence of a
functor between two categories of ``generalized topological spaces'', one with
points (Basic Pairs) and one point-free (Basic Topologies).
The formalization has been commissioned by the inventor of the theory, Giovanni
Sambin, to verify in what sense and with what difficulties his theory was
``implementable'' and to check that all intermediate constructions respect the
stringent size requirements imposed by predicative logic. Hence, the
formalization is quite unusual since it has to make explicit all size
information that is often hidden as much as possible.
The version of the system we used for the formalization was largely sub-optimal
for the task and the formalization drove several major improvements of the
system that will be integrated in the next major forthcoming release of Matita,
version 1.0. In this paper we show the motivating examples for the
improvements, taken directly from the formalization; then we describe a
possible sub-optimal solution in Matita ½, that is probably
exploitable in other systems too, and we hint at the better solution available
in Matita 1.0.
Most notable features motivated by this formalization are unification hints,
non uniform coercions, explicit checked universes in the style of Courant and
separated hierarchies for predicative propositions and data types allowing a
controlled use of the type theoretic Axiom of Choice as in Maietti-Sambin.
Superposition as a logical glue
with Andrea Asperti. Published
in the proceedings of TYPES 2009, EPTCS
Volume 53, Pages 1-15, Year 2011, ISSN: 2075-2180, DOI: 10.4204/EPTCS.53.
Download
See abstract
Abstract: The typical mathematical language systematically exploits
notational and logical abuses whose resolution requires not just the knowledge
of domain specific notation and conventions, but not trivial skills in the
given mathematical discipline. A large part of this background knowledge is
expressed in form of equalities and isomorphisms, allowing mathematicians to
freely move between different incarnations of the same entity without even
mentioning the transformation. Providing ITP-systems with similar capabilities
seems to be a major way to improve their intelligence, and to ease the
communication between the user and the machine. The present paper discusses our
experience of integration of a superposition calculus within the Matita
interactive prover, providing in particular a very flexible, ``smart''
application tactic, and a simple, innovative approach to automation.
Nonuniform Coercions via Unification Hints
with Claudio Sacerdoti Coen. Published
in the proceedings of TYPES 2009, EPTCS
Volume 53, Pages 16-29, Year 2011, ISSN: 2075-2180, DOI: 10.4204/EPTCS.53.
Download
Slides
See abstract
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.
Smart Matching
with Andrea Asperti.
Published in the proceedings of MKM2010, LNCS, Volume 6167/2010, Year 2010,
Pages 263-277, DOI 10.1007/978-3-642-14128-7_23, ISBN 978-3-642-14127-0
Download
See abstract
Abstract: One of the most annoying aspects in the formalization of
mathematics is the need of transforming notions to match a given, existing
result. This kind of transformations, often based on a conspicuous background
knowledge in the given scientific domain (mostly expressed in the form of
equalities or isomorphisms), are usually implicit in the mathematical
discourse, and it would be highly desirable to obtain a similar behavior in
interactive provers. The paper describes the superposition-based implementation
of this feature inside the Matita interactive theorem prover, focusing in
particular on the so called smart application tactic, supporting smart matching
between a goal and a given result.
A new type for tactics
with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen.
To appear in the proceedings of ACM SIGSAM PLMMS 2009,
ISBN 978-1-60558-735-6.
Published as technical report UBLCS-2009-14.
Download
Slides
See abstract
The type of tactics in all (procedural) proof assistants is (a variant of)
the one introduced in LCF. We discuss why this is inconvenient and we propose
a new type for tactics that 1) allows the implementation of more clever
tactics; 2) improves the implementation of declarative languages on top
of procedural ones; 3) allows for better proof structuring; 4) improves
proof automation; 5) allows tactics to rearrange and delay the goals to be
proved (e.g. in case of side conditions or PVS subtyping judgements).
Hints in Unification
with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen.
Published in the proceedings of TPHOLs 2009, LNCS, Volume 5674/2009,
Pages 84-98, DOI 10.1007/978-3-642-03359-9, ISBN 978-3-642-03358-2
Download
Slides
See 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.
Natural deduction environment for Matita
with Claudio Sacerdoti Coen.
Published in the proceedings of MKM2009, Volume 5625, Pages 486-491,
ISBN 978-3-642-02613-3, DOI 10.1007/978-3-642-02614-0_40
Download
Slides
See 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 compact kernel for the calculus of inductive constructions
with Andrea Asperti, Wilmer Ricciotti and Claudio Sacerdoti Coen.
Published in the Journal Sadhana,
Volume 34, Pages 71-144, Year 2009. ISSN: 0256-2499
Download
Slides
See 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.
A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
with Claudio Sacerdoti Coen.
Published by the Journal of Formalized Reasoning
, Issue 1, Volume 1, Pages 51-89, Year 2008. ISSN: 1972-5787.
Download
See 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.
An interactive driver for goal directed proof
strategies
with Andrea Asperti.
Published in the Proceedings of
UITP 2008:
8th International Workshop On
User Interfaces for Theorem Provers, 22 August 2008, Montréal, Québec, Canada. ENTCS, Volume 226, 3 January 2009, Pages 89-105, ISSN 1571-0661,
DOI 10.1016/j.entcs.2008.12.099
Download
Slides
See abstract
Interactive Theorem Provers (ITPs) are tools meant to assist the user
during the formal development of mathematics. Automatic proof
searching procedures are a desirable aid, and most ITPs supply the
user with an extensive set of facilities to improve automation.
However, the black-box nature of most automatic procedure conflicts
with the interactive nature of these tools: a newcomer running an automatic
procedure learns nothing by its execution (especially in case of failure),
and a trained user has no opportunities to interactively guide
the procedure towards the solution, e.g. pruning wrong or not
promising branches of the search tree.
In this paper we discuss the implementation of the resolution based
automatic procedure of the Matita ITP, explicitly
conceived to be interactively driven by the user through a suitable,
simple graphical interface.
Working with Mathematical Structures in Type Theory
with Sacerdoti Coen.
Published in the 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.
Download
Slides
See 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 and 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.
A modular formalisation of finite group theory
with Georges Gonthier, Assia Mahboubi , Laurence Rideau and Laurent Thery.
Published in the Proceedings of
TPHOL 2007: The 20th International
Conference on Theorem Proving in Higher Order Logics. LNCS, Volume 4732, ISBN: 978-3-540-74590-7, DOI: 10.1007/978-3-540-74591-4, Pages: 86-101, 2007.
Download
See abstract
In this paper, we present a formalisation of elementary group theory done in
Coq. This work is the first milestone of a long-term effort to
formalise Feit-Thompson theorem. As our further developments will heavily
rely on this initial base, a special care has been taken to articulate it in
the most compositional way.
Higher order proof reconstruction from paramodulation-based refutations: the unit equality case
with Andrea Asperti.
Published in the Proceedings of MKM 2007: The 6th International Conference on Mathematical Knowledge Management. LNAI, Volume 4573, ISBN: 978-3-540-73083-5, 2007.
Download
Slides
See abstract
In this paper we address the problem of reconstructing a higher order,
checkable proof object starting from a proof trace left by a first order
automatic proof searching procedure, in a restricted equational framework.
The automatic procedure is based on superposition rules for the unit
equality case. Proof transformation techniques aimed to improve the
readability of the final proof are discussed.
Crafting a Proof Assistant
with Andrea Asperti, Claudio Sacerdoti Coen, Stefano Zacchiroli.
Published in the Proceedings of
Types 2006: Conference of the Types Project.
Nottingham, UK -- April 18-21, 2006. LNCS Volume 4502, Springer Berlin / Heidelberg, ISBN 978-3-540-74463-4, pp. 18-32, 2007.
Download
Slides
See 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.
User Interaction with the Matita Proof Assistant
with Andrea Asperti, Claudio Sacerdoti Coen, Stefano Zacchiroli.
Published in the
Journal of Automated Reasoning,
Special Issue
on User Interfaces for Theorem Proving,
Springer Netherlands, ISSN 0168-7433, Volume 39, Issue 2, August 2007,
Pages: 109-139.
Download
See abstract
Matita is a new, document-centric, tactic-based interactive theorem prover
under development at the University of Bologna. 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 (MathML-based) notational rendering, and
the complex interplay between syntax, presentation, and semantics (e.g. for
disambiguation of formulae input by the user, and direct manipulation of
terms).
Tinycals: Step by Step Tacticals
with Claudio Sacerdoti Coen, Stefano Zacchiroli.
In Proceedings of UITP 2006:
User Interfaces for Theorem Provers.
Seattle, WA -- August 21, 2006. ENTCS, Volume 174, Issue 2 (May 2007),
Pages 125 - 142, ISSN:1571-0661
Download
Slides
See 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 the Matita proof assistant.
Modified Realizability and Inductive Types
with Andrea Asperti, June 2006. Technical report [UBLCS-2006-18][tr200618].
Download
See abstract
In 1959, Kreisel introduced a notion of modified realizability that,
among other things, provides an alternative technique to Godel functional
(dialectica) interpretation for establishing the connection between Peano
Arithmetic and System T. In this paper we give a modern presentation of
modified realizability, and generalize it to arbitrary inductive types in a
first order setting and their extension with strong elimination rules.
A content based mathematical search engine: Whelp
with Andrea Asperti, Ferruccio Guidi, Claudio Sacerdoti Coen, and Stefano
Zacchiroli.
Published In Proceedings of TYPES 2004
conference: Types for Proofs and Programs.
Paris, France -- December 15-18, 2004. LNCS 3839, Springer Berlin /
Heidelberg, ISBN 3-540-31428-8,
pp. 17-32, 2006.
Download
See 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.
User Level Networking-Personal IP: assigning each
user his/her own IP addresses in multiuser operating systems
with Alessandro Pira and Renzo Davoli.
Published in the proceedings of ICN04,
IEEE International Conference on Networking,
February 29 - March 4 2004,
Guadeloupe, French Caribbean.
Download
See abstract
When a user logs into a machine using User Level Networking-Personal IP
he/she can be assigned a personal IP address, a set of personal IP addresses,
or no address at all. In a multiuser multitasking operating system where
several users are operating at the same time, each user has his/her own
personalized access to the network. In this way the system and network
administrator can assign access rights, traffic shaping and routing on a
user-by-user basis. In cases of user abuses on the network there is direct
mapping between the IP address and his/her user id; it is sufficient to read
a single log file.
Dissertations
Interactive Theorem Provers: issues faced as a user and tackled as a developer
Technical report UBLCS-2008-03
Download
See abstract
Interactive theorem provers (ITP for short) are tools whose final aim is to
certify proofs written by human beings. To reach that objective they have to
fill the gap between the high level language used by humans for communicating
and reasoning about mathematics and the lower level language that a machine
is able to understand and process. The user perceives this gap in terms
of missing features or inefficiencies. The developer tries to accommodate
the user requests without increasing the already high complexity of these
applications. We believe that satisfactory solutions can only come from a
strong synergy between users and developers. We devoted most part of our PHD
designing and developing the Matita interactive theorem prover. The software
was born in the computer science department of the University of Bologna as
the result of composing together all the technologies developed by the HELM
team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at
giving accessibility through the web to the libraries of formalised
mathematics of various interactive theorem provers, taking Coq as the main
test case. The motivations for giving life to a new ITP are:
- study
the architecture of these tools, with the aim of understanding the source of
their complexity.
- exploit such a knowledge to experiment new
solutions that, for backward compatibility reasons, would be hard (if not
impossible) to test on a widely used system like Coq.
Matita is
based on the Curry-Howard isomorphism, adopting the Calculus of Inductive
Constructions (CIC) as its logical foundation. Proof objects are thus, at
some extent, compatible with the ones produced with the Coq ITP, that is
itself able to import and process the ones generated using Matita. Although
the systems have a lot in common, they share no code at all, and even most of
the algorithmic solutions are different. The thesis is composed of two parts
where we respectively describe our experience as a user and a developer of
interactive provers. In particular, the first part is based on two different
formalisation experiences:
- our internship in the Mathematical
Components team (INRIA), that is formalising the finite group theory required
to attack the Feit Thompson Theorem. To tackle this result, giving an
effective classification of finite groups of odd order, the team adopts the
SSR Coq extension, developed by Georges Gonthier for the proof of the four
colours theorem.
- our collaboration at the D.A.M.A. Project, whose
goal is the formalisation of abstract measure theory in Matita leading to
a constructive proof of Lebesgue's Dominated Convergence Theorem.
The most notable issues we faced, analysed in this part of the thesis, are
the following: the difficulties arising when using black box automation
in large formalisations; the impossibility for a user (especially a newcomer)
to master the context of a library of already formalised results; the
uncomfortable big step execution of proof commands historically adopted in
ITPs; the difficult encoding of mathematical structures with a notion of
inheritance in a type theory without subtyping like CIC. In the second part
of the manuscript many of these issues will be analysed with the looking
glasses of an ITP developer, describing the solutions we adopted in the
implementation of Matita to solve these problems: integrated searching
facilities to assist the user in handling large libraries of formalised
results; a small step execution semantic for proof commands; a flexible
implementation of coercive subtyping allowing multiple inheritance with
shared substructures; automatic tactics, integrated with the searching
facilities, that generates proof commands (and not only proof objects,
usually kept hidden to the user) one of which specifically designed to be
user driven.