An intuitionistic set-theoretical model of fully dependent CC

DOI10.1017/s0960129523000087arXiv2010.12504MaRDI QIDQ6174091

Jacques Garrigue, Masahiro Sato

Publication date: 13 July 2023

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2010.12504

zbMATH Keywords

intuitionistic logictype theorymodel

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• The calculus of constructions
• Sheaves in geometry and logic: a first introduction to topos theory
• Categorical logic and type theory
• A higher-order calculus and theory abstraction
• Proof-irrelevant model of CC with predicative induction and judgmental equality
• On the strength of proof-irrelevant type theories
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A simple model construction for the Calculus of Constructions
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus
• Introduction to generalized type systems
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: An intuitionistic set-theoretical model of fully dependent CC