An intuitionistic set-theoretical model of fully dependent CC

DOI10.1017/S0960129523000087MaRDI QIDQ6174091FDO

Authors Masahiro Sato, Jacques Garrigue

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

modelintuitionistic logictype theory

Mathematics Subject Classification ID

Computer science (68-XX)

Abstract: Werner's set-theoretical model is one of the simplest models of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. However this model of Prop is so coarse that the principle of excluded middle holds. Following our previous work, we interpret Prop into a topological space (a special case of Heyting algebra) to make the model more intuitionistic without sacrificing simplicity. We improve on that work by providing a full interpretation of dependent product types, using Alexandroff spaces. We also extend our approach to inductive types by adding support for lists.

Cites work

• scientific article; zbMATH DE number 1722653 (Why is no real title available?)
• scientific article; zbMATH DE number 3882404 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1303733 (Why is no real title available?)
• scientific article; zbMATH DE number 1332362 (Why is no real title available?)
• scientific article; zbMATH DE number 1028819 (Why is no real title available?)
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 2003160 (Why is no real title available?)
• scientific article; zbMATH DE number 1420782 (Why is no real title available?)
• scientific article; zbMATH DE number 226803 (Why is no real title available?)
• A general formulation of simultaneous inductive-recursive definitions in type theory
• A higher-order calculus and theory abstraction
• A simple model construction for the calculus of constructions
• Categorical logic and type theory
• Homotopy type theory. Univalent foundations of mathematics
• Introduction to generalized type systems
• On the strength of proof-irrelevant type theories
• Proof-irrelevant model of CC with predicative induction and judgmental equality
• Sets in Coq, Coq in Sets
• Sheaves in geometry and logic: a first introduction to topos theory
• The calculus of constructions
• Theoretical Pearls:Representing ‘undefined’ in lambda calculus

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

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