MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Basin, David A.
Howe, D.		dblp
dblp
Editor(s):
Ito, T.
Meyer, A. R.		dblp
dblp
BibTeX cite key*:
Basin91a
Title, Booktitle
Title*:
Some Normalization Properties of Martin-Löf's Type Theory, and Applications
Booktitle*:
International Conference on Theoretical Aspects of Computer Software (TACS '91)
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Sendai, Japan
Language:
English
Event Date*
(no longer used):
September 24-27
Organization:
Event Start Date:
21 May 2024
Event End Date:
21 May 2024
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
526
Number:
Month:
Pages:
475-494
Year*:
1991
VG Wort Pages:
ISBN/ISSN:
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
For certain kinds of applications of type theories, the faithfulness of formalization in the theory depends on intensional, or structural, properties of objects constructed in the theory. For type theories such as LF, such properties can be established via an analysis of normal forms and types. In type theories such as Nuprl or Martin-L\"of's polymorphic type theory, which are much more expressive than LF, the underlying programming language is essentially untyped, and terms proved to be in types do not necessarily have normal forms. Nevertheless, it is possible to show that for Martin-L\"of's type theory, and a large class of extensions of it, a sufficient kind of normalization property does in fact hold in certain well-behaved subtheories. Applications of our results include the use of the type theory as a logical framework in the manner of LF, and an extension of the {\em proofs-as-programs} paradigm to the synthesis of verified computer hardware. For the latter application we point out some advantages to be gained by working in a more expressive
type theory.
Download
Access Level:

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:



BibTeX Entry:
@INPROCEEDINGS{Basin91a,
AUTHOR = {Basin, David A. and Howe, D.},
 EDITOR = {Ito, T. and Meyer, A. R.},
 TITLE = {Some Normalization Properties of Martin-L{\"o}f's Type Theory, and Applications},
 BOOKTITLE = {International Conference on Theoretical Aspects of Computer Software (TACS '91)},
 PUBLISHER = {Springer},
 YEAR = {1991},
 VOLUME = {526},
 PAGES = {475--494},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Sendai, Japan},
}

Entry last modified by Uwe Brahm, 08/07/2014
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]		Created
01/14/1995 06:50:44 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE
Uwe Brahm/MPII/DE		Edit Dates
03/27/98 09:57:39 PM
03/27/98 09:56:08 PM
21/01/95 21:22:47
21/01/95 20:45:25
17/01/95 19:26:27