An intuitionistic theory of types with assumptions of high-arity variables

DOI10.1016/0168-0072(92)90023-SzbMath0785.03039MaRDI QIDQ1192333

Annalisa Bossi, Silvio Valentini

Publication date: 27 September 1992

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

zbMATH Keywords

normal form theoremcorrect programcanonical form theoremcomputational interpretation of typeshigh-arity variablesMartin-Löf's intuitionistic theory of types

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) General topics in the theory of software (68N01) Second- and higher-order arithmetic and fragments (03F35)

Related Items (2)

An intuitionistic theory of types with assumptions of high-arity variables ⋮ MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Telescopic mappings in typed lambda calculus
• Propositions and specifications of programs in Martin-Löf's type theory
• Do-it-yourself type theory
• On the syntax of Martin-Löf's type theories
• The lambda calculus, its syntax and semantics
• An intuitionistic theory of types with assumptions of high-arity variables
• Writing programs that construct proofs
• Constructive mathematics and computer programming
• Program derivation in type theory: A partitioning problem
• Intensional interpretations of functionals of finite type I

This page was built for publication: An intuitionistic theory of types with assumptions of high-arity variables