scientific article; zbMATH DE number 65535

zbMATH Open0755.03033MaRDI QIDQ4012883FDOQ4012883

Authors: Peter Dybjer 

Publication date: 27 September 1992

Title of this publication is not available (Why is that?)

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

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)

Cited In (32)

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

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)