Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:




Library Locked Library locked




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

URL of the conference:


URL for downloading the paper:


Event Address*:

Sendai, Japan

Language:

English

Event Date*
(no longer used):

September 24-27

Organization:


Event Start Date:

22 September 2019

Event End Date:

22 September 2019

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
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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