scientific article
From MaRDI portal
Publication:4012883
zbMath0755.03033MaRDI QIDQ4012883
Publication date: 27 September 1992
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
polymorphismMartin-Löf's type theoryprimitive recursive functionssimply typed \(\lambda\)-calculusinductive setsinductive familiesprimitive recursive families of functions
Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Related Items (22)
Finitary higher inductive types in the groupoid model ⋮ Inductive families ⋮ Innovations in computational type theory using Nuprl ⋮ Constructive sets in computable sets ⋮ A type theoretic interpretation of constructive domain theory ⋮ Representing inductively defined sets by wellorderings in Martin-Löf's type theory ⋮ Expressing computational complexity in constructive type theory ⋮ Induction-recursion and initial algebras. ⋮ Cumulative Inductive Types in Coq ⋮ How to Reason Coinductively Informally ⋮ Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids ⋮ Semantics of constructions. I: The traditional approach ⋮ Transitivity in coercive subtyping ⋮ Dependent Types at Work ⋮ Coercion completion and conservativity in coercive subtyping ⋮ Type Theory Should Eat Itself ⋮ A fixedpoint approach to implementing (Co)inductive definitions ⋮ Lexicographic Path Induction ⋮ A note on complexity measures for inductive classes in constructive type theory ⋮ Indexed induction-recursion ⋮ Lightweight Static Capabilities ⋮ Free Theorems and Runtime Type Representations
This page was built for publication:
