Constructive natural deduction and its ‘ω-set’ interpretation

DOI10.1017/S0960129500001298zbMath0756.03028MaRDI QIDQ4006232

Eugenio Moggi

Publication date: 26 September 1992

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

zbMATH Keywords

constructive type theorysemantics\(\lambda\)-calculusexpressive powersyntaxpropositions-as-typesmodest sets\(\omega\)-setsexplicit polymorphism

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items (26)

A computable expression of closure to efficient causation ⋮ Maps. I: Relative to a factorisation system ⋮ The S-replete construction ⋮ On completeness and cocompleteness in and around small categories ⋮ Constructive sets in computable sets ⋮ On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory ⋮ Covariant types ⋮ Revisiting the notion of function ⋮ Conservativity between logics and typed λ calculi ⋮ Internal models of system F for decompilation ⋮ Alpha conversion, conditions on variables and categorical logic ⋮ Bifibrational functorial semantics of parametric polymorphism ⋮ A modest model of records, inheritance, and bounded quantification ⋮ Relations in operational categories ⋮ Categorical models of polymorphism ⋮ A simple model construction for the Calculus of Constructions ⋮ Comprehension categories and the semantics of type dependency ⋮ Semantics of constructions. I: The traditional approach ⋮ Computability structures, simulations and realizability ⋮ Unnamed Item ⋮ Functorial polymorphism ⋮ From exact sciences to life phenomena: Following Schrödinger and Turing on programs, life and causality ⋮ From constructivism to computer science ⋮ Formal parametric polymorphism ⋮ The genericity theorem and parametricity in the polymorphic \(\lambda\)- calculus ⋮ An exactification of the monoid of primitive recursive functions

Cites Work

• Unnamed Item
• Unnamed Item
• Computability in higher types, P\(\omega\) and the completeness of type assignment
• Completeness of type assignment in continuous lambda models
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• Polymorphic type inference and containment
• Intuitionist type theory and the free topos
• LCF considered as a programming language
• A theory of type polymorphism in programming
• The completeness theorem for typing lambda-terms
• A filter lambda model and the completeness of type assignment
• The Discrete Objects in the Effective Topos
• Data Types as Lattices
• The Principal Type-Scheme of an Object in Combinatory Logic

This page was built for publication: Constructive natural deduction and its ‘ω-set’ interpretation