Impredicativity entails untypedness

DOI10.1017/S0960129502003663zbMath1001.03013MaRDI QIDQ3146246

Thomas Streicher, Peter Lietz

Publication date: 31 October 2002

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

zbMATH Keywords

partial combinatory algebrarealizability toposrealizability modelsimpredicative type theorycategory of assembliesuniversal type

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Combinatory logic and lambda calculus (03B40)

Related Items (9)

Converse extensionality and apartness ⋮ A synthetic theory of sequential domains ⋮ Constructive toposes with countable sums as models of constructive set theory ⋮ Characterizing partitioned assemblies and realizability toposes ⋮ Coherence Spaces and Uniform Continuity ⋮ On the ubiquity of certain total type structures ⋮ Introduction to Turing categories ⋮ A characterization of the left exact categories whose exact completions are toposes ⋮ More exact completions that are toposes

This page was built for publication: Impredicativity entails untypedness