Extensional and Intensional Semantic Universes

DOI10.1145/3209108.3209206zbMATH Open1452.03032OpenAlexW2798011798MaRDI QIDQ5145281FDOQ5145281

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

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
• Denotational semantics for intuitionistic type theory using a hierarchy of domains with totality

Mathematics Subject Classification ID

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

Cited In (4)

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

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)