scientific article; zbMATH DE number 65535

MaRDI QIDQ4012883zbMATH OpenFDO

Authors Peter Dybjer

Publication date 27 September 1992

zbMATH Keywords

polymorphismprimitive recursive functionssimply typed \(\lambda\)-calculusinductive setsinductive familiesMartin-Löf's type theoryprimitive recursive families of functions

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Inductive families
• Remarks on Martin-Löf's partial type theory
• scientific article; zbMATH DE number 2077110
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• scientific article; zbMATH DE number 1302063

Cited in

(32)

• On the syntax of Martin-Löf's type theories
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• A Comparison of Type Theory with Set Theory
• Semantics of constructions. I: The traditional approach
• Transitivity in coercive subtyping
• Constructive sets in computable sets
• A note on complexity measures for inductive classes in constructive type theory
• scientific article; zbMATH DE number 3938546 (Why is no real title available?)
• An information system interpretation of Martin-Löf's partial type theory with universes
• scientific article; zbMATH DE number 2077110 (Why is no real title available?)
• A type theoretic interpretation of constructive domain theory
• Propositional functions and families of types
• Inductive families
• Lightweight static capabilities
• Indexed induction-recursion
• Characterizing the interpretation of set theory in Martin-Löf type theory
• Innovations in computational type theory using Nuprl
• Finitary higher inductive types in the groupoid model
• Lexicographic Path Induction
• Martin-Löf's type theory as an open-ended framework
• A fixedpoint approach to implementing (co)inductive definitions
• How to reason coinductively informally
• Induction-recursion and initial algebras.
• Dependent Types at Work
• Cumulative inductive types in Coq
• scientific article; zbMATH DE number 517090 (Why is no real title available?)
• Expressing computational complexity in constructive type theory
• Free theorems and runtime type representations
• Coercion completion and conservativity in coercive subtyping
• Type theory should eat itself
• Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
• scientific article; zbMATH DE number 3985206 (Why is no real title available?)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4012883)