- Certificates for Incremental Type Checking
- Puech, Matthias <1983>
Subject
- INF/01 Informatica
Description
- The central topic of this thesis is the study of algorithms for type checking, both from the programming language and from the proof-theoretic point of view. A type checking algorithm takes a program or a proof, represented as a syntactical object, and checks its validity with respect to a specification or a statement. It is a central piece of compilers and proof assistants. We postulate that since type checkers are at the interface between proof theory and program theory, their study can let these two fields mutually enrich each other. We argue by two main instances: first, starting from the problem of proof reuse, we develop an incremental type checker; secondly, starting from a type checking program, we evidence a novel correspondence between natural deduction and the sequent calculus.
Date
- 2013-04-08
Type
- Doctoral Thesis
- PeerReviewed
Format
- application/pdf
Identifier
urn:nbn:it:unibo-10396
Puech, Matthias (2013) Certificates for Incremental Type Checking , [Dissertation thesis], Alma Mater Studiorum Università di Bologna. Dottorato di ricerca in Informatica