transparent gif

 

Ej inloggad.

Göteborgs universitets publikationer

Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs

Författare och institution:
Andreas Abel (-); Thierry Coquand (Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU))
Publicerad i:
Fundamenta Informaticae, 77 ( 4 ) s. 345-395
ISSN:
0169-2968
Publikationstyp:
Artikel, refereegranskad vetenskaplig
Publiceringsår:
2007
Språk:
engelska
Sammanfattning (abstract):
Martin-Löf's Logical Framework is extended by strong Sigma-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped beta eta-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with eta-equality on beta-normal forms, which is shown equivalent to the algorithmic equality.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
NATURVETENSKAP ->
Data- och informationsvetenskap
Nyckelord:
lambda-calculus
Postens nummer:
175708
Posten skapad:
2013-04-15 10:51
Posten ändrad:
2016-06-23 15:11

Visa i Endnote-format

Göteborgs universitet • Tel. 031-786 0000
© Göteborgs universitet 2007