An intuitionistic theory of types with assumptions of high-arity variables
type: Item
instance of: scholarly article
title: An intuitionistic theory of types with assumptions of high-arity variables
zbMATH Open document ID: 0785.03039
DOI: 10.1016/0168-0072(92)90023-S
published in: Annals of Pure and Applied Logic
publication date: 1992-09-27T00:00:00Z
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 60738
zbMATH Keywords: Martin-Löf's intuitionistic theory of types
zbMATH Keywords: high-arity variables
zbMATH Keywords: normal form theorem
zbMATH Keywords: canonical form theorem
zbMATH Keywords: computational interpretation of types
zbMATH Keywords: correct program
author: Annalisa Bossi
author: Silvio Valentini
MaRDI profile type: Publication
cites work: Do-it-yourself type theory
cites work: The lambda calculus, its syntax and semantics
cites work: Writing programs that construct proofs
cites work: Q3914980
cites work: Telescopic mappings in typed lambda calculus
cites work: Q5638283
cites work: Q4099613
cites work: Constructive mathematics and computer programming
cites work: Q3999860
cites work: Propositions and specifications of programs in Martin-Löf's type theory
cites work: Program derivation in type theory: A partitioning problem
cites work: Q5559220
cites work: Intensional interpretations of functionals of finite type I
cites work: On the syntax of Martin-Löf's type theories
description: scientific article; zbMATH DE number 60738