© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Abstract interpretation of constructive type theory
Alastair Telford and Simon Thompson
Technical Report 19-96*, University of Kent, Computing Laboratory, University of Kent, Canterbury, UK, October 1996.Abstract
Constructive type theories, such as that of Martin-Lof, allow program construction and verification to take place within a single system: proofs may be read as programs and propositions as types. However, parts of proofs may be seen to be irrelevant from a computational viewpoint. We show how a form of abstract interpretation may be used to detect computational redundancy in a functional language based upon Martin-Lof's type theory. Thus, without making any alteration to the system of type theory itself, we present an automatic way of discovering and removing such redundancy. We also note that the strong normalisation property of type theory means that proofs of correctness of the abstract interpretation are simpler, being based upon a set-theoretic rather than a domain-theoretic semantics.
Keywords: Type theory, functional programming, computational redundancy, abstract interpretation.
Download publication
136 kbytes
Bibtex Record
@techreport{41,
author = {Alastair Telford and Simon Thompson},
title = {Abstract Interpretation of Constructive Type Theory},
month = {October},
year = {1996},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1996/41},
address = {University of Kent, Canterbury, UK},
hensa_abstractfilename = {pub/misc/ukc.reports/comp.sci/abstracts/19-96},
hensa_ftpaddress = {unix.hensa.ac.uk},
hensa_reportfilename = {pub/misc/ukc.reports/comp.sci/reports/19-96.ps.Z},
institution = {University of Kent, Computing Laboratory},
number = {19-96*},
}