Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/405

This item has been viewed 22 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
ECS-LFCS-94-304.dviTeX DVI file667.21 kBTeX dviView/Open
ECS-LFCS-94-304.PDFAdobe PDF10.23 MBAdobe PDFView/Open
ECS-LFCS-94-304.psPostScript file1.22 MBPostscriptView/Open
Title: A Typed Operational Semantics for Type Theory
Authors: Goguen, Healfdene
Supervisor(s): Burstall, Rod
Luo, Zhaohui
Issue Date: Jul-1994
Publisher: University of Edinburgh. College of Science and Engineering. School of Informatics.
Abstract: Untyped reduction provides a natural operational semantics for type theory. Normalization results say that such a semantics is sound. However, this reduction does not take type information into account and gives no information about canonical forms for terms. We introduce a new operational semantics, which we call typed operational semantics, which defines a reduction to normal form for terms which are well-typed in the type theory. The central result of the thesis is soundness of the typed operational semantics for the original system. Completeness of the semantics is straightforward. We demonstrate that this equivalence between the declarative and operational presentations of type theory has important metatheoretic consequences: results such as strengthening, subject reduction and strong normalization follow by straightforward induction on derivations in the new system. We introduce these ideas in the setting of the simply typed lambda calculus. We then extend the techniques to Luo's system UTT, which is Martin-Löf's Logical Framework extended by a general mechanism for inductive types, a predicative universe and an impredicative universe of propositions. We also give a proof-irrelevant set-theoretic semantics for UTT.
URI: http://hdl.handle.net/1842/405
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy