Computational adequacy for recursive types in models of intuitionistic set theory

DOI10.1016/j.apal.2003.12.005zbMath1056.03015OpenAlexW2094544397MaRDI QIDQ1886324

Alex K. Simpson

Publication date: 18 November 2004

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/12288570/cartinmist.pdf

zbMATH Keywords

Domain theoryAlgebraic compactnesscategorical models of intuitionistic set theoryFPCinterpretation of recursive typesrecursively typed lambda-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Categorical logic, topoi (03G30) Topoi (18B25) Nonclassical and second-order set theories (03E70) Combinatory logic and lambda calculus (03B40)

Related Items

Computational adequacy for recursive types in models of intuitionistic set theory, Relating first-order set theories, toposes and categories of classes, Weighted models for higher-order computation, Relating First-Order Set Theories and Elementary Toposes, Intuitionistic fixed point logic, Synthetic domain theory and models of linear Abadi {\&} Plotkin logic, A Brief Introduction to Algebraic Set Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A presentation of the initial lift-algebra
• Sheaves in geometry and logic: a first introduction to topos theory
• Extensional PERs
• LCF considered as a programming language
• Categorical logic and type theory
• From term models to domains
• Semantics of weakening and contraction
• Axioms and (counter)examples in synthetic domain theory
• Computational adequacy for recursive types in models of intuitionistic set theory
• Relational properties of domains
• Tripos theory
• The Category-Theoretic Solution of Recursive Domain Equations
• General synthetic domain theory – a logical approach
• Building domains from graph models
• A uniform approach to domain theory in realizability models
• Axiomatic Domain Theory in Categories of Partial Maps
• Domains in \(H\)