Till sidans topp

Sidansvarig: Webbredaktion
Sidan uppdaterades: 2012-09-11 15:12

Tipsa en vän
Utskriftsversion

An Adequacy Theorem for D… - Göteborgs universitet Till startsida
Webbkarta
Till innehåll Läs mer om hur kakor används på gu.se

An Adequacy Theorem for Dependent Type Theory

Artikel i vetenskaplig tidskrift
Författare Thierry Coquand
Simon Huber
Publicerad i Theory of Computing Systems
Volym 63
Nummer/häfte 4
Sidor 647-665
ISSN 1432-4350
Publiceringsår 2019
Publicerad vid Institutionen för data- och informationsteknik (GU)
Sidor 647-665
Språk en
Länkar dx.doi.org/10.1007/s00224-018-9879-...
Ämnesord Dependent type theory, Domain theory, Finitary projections, Computer Science, Mathematics
Ämneskategorier Datavetenskap (datalogi)

Sammanfattning

We present a domain model of dependent type theory and use it to prove basic metatheoretic properties. In particular, we prove that two convertible terms have the same Bohm tree. The method used is reminiscent of the use of "inclusive predicates" in domain theory.

Sidansvarig: Webbredaktion|Sidan uppdaterades: 2012-09-11
Dela:

På Göteborgs universitet använder vi kakor (cookies) för att webbplatsen ska fungera på ett bra sätt för dig. Genom att surfa vidare godkänner du att vi använder kakor.  Vad är kakor?