An adequacy theorem for dependent type theory

DOI10.1007/S00224-018-9879-9MaRDI QIDQ2311883zbMATH OpenOpenAlexFDO

Authors Thierry Coquand, Simon Huber

Publication date 4 July 2019

Published in Theory of Computing Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s00224-018-9879-9

zbMATH Keywords

dependent type theorydomain theoryfinitary projections

Mathematics Subject Classification ID

Type theory (03B38)

Recommendations

• Density theorems for the domains-with-totality semantics of dependent types
• scientific article; zbMATH DE number 1302058
• Dependence and independence results for (impredicative) calculi of dependent types
• scientific article; zbMATH DE number 1241699
• Games for dependent types

Cites work

• Domain interpretations of Martin-Löf's partial type theory
• Domain theoretic models of polymorphism
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 3783068 (Why is no real title available?)
• scientific article; zbMATH DE number 65534 (Why is no real title available?)
• scientific article; zbMATH DE number 3490449 (Why is no real title available?)
• On irrelevance and algorithmic equality in predicative type theory
• Proofs and computations
• Pure type system conversion is always typable
• Pure type systems with judgemental equality
• Remarks on Martin-Löf's partial type theory

Cited in

(5)

• On generically stable types in dependent theories
• Independence results for calculi of dependent types
• Type-theory in color
• Computer Science Logic
• Stable domination and weight

This page was built for publication: An adequacy theorem for dependent type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2311883)