Adequate encodings of logical systems in UTT

Mylonakis Pascual, Nicolás

View/Open

R00-18.pdf (199,5Kb)

View UPCommons Usage Statistics

LA Referencia / Recolecta stats

Cita com:

Show full item record

Mylonakis Pascual, Nicolás

Document typeResearch report

Defense date2003-03-02

Rights accessOpen Access

All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder

Abstract

In this paper, we present an existing and formalized type theory (UTT) as a logical framework. We compare the resulting framework with LF and give the representation of two significant type systems in the framework: the typed lambda calculus which is closely related to higher-order logic and a linear type system which is not possible to encode in LF.

CitationMylonakis, N. "Adequate encodings of logical systems in UTT". 2003.

Is part ofR00-18

URIhttp://hdl.handle.net/2117/95872

Collections

Departament de Ciències de la Computació - Reports de recerca [1.108]

View UPCommons Usage Statistics

Show full item record

Files	Description	Size	Format	View
R00-18.pdf		199,5Kb	PDF	View/Open

UPCommons. Global access to UPC knowledge

Adequate encodings of logical systems in UTT

View/Open

Browse