Extensional and Intensional Semantic Universes

DOI10.1145/3209108.3209206MaRDI QIDQ5145281zbMATH OpenOpenAlexFDO

Authors Valentin Blot, Jim Laird

Publication date 20 January 2021

Published in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3209108.3209206

Mathematics Subject Classification ID

Type theory (03B38) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Formalizing semantic bidirectionalization and extensions with dependent types
• Intensional models for the theory of types
• Extensional constructs in intensional type theory
• scientific article; zbMATH DE number 1678369
• A general semantic construction of dependent refinement type systems, categorically
• A relationally parametric model of dependent type theory
• EXTENSIONAL REALIZABILITY AND CHOICE FOR DEPENDENT TYPES IN INTUITIONISTIC SET THEORY
• Semantic types: a fresh look at the ideal model for types
• scientific article; zbMATH DE number 6680163
• Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality

Cited in

(4)

• Game semantics for dependent types
• Dependent event types
• Games for dependent types
• Game semantics of Martin-Löf type theory

This page was built for publication: Extensional and Intensional Semantic Universes

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