Logical relations and inductive/coinductive types

DOI10.1007/10703163_23MaRDI QIDQ4263807zbMATH OpenFDO

Authors Thorsten Altenkirch

Publication date 25 April 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/10703163_23

zbMATH Keywords

lambda-calculus with positive inductive and coinductive typesmonotone inductive definitionsnatural transformationsrepresentable functorsterms of functorial type

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Logical relations for monadic types
• scientific article; zbMATH DE number 1948186
• Inductive Type Schemas as Functors
• Inductive, coinductive, and pointed types
• Logical relations and the typed λ-calculus

Cited in

(13)

• Iteration and coiteration schemes for higher-order and nested datatypes
• Inductive, coinductive, and pointed types
• Relations Versus Functions at the Foundations of Logic: Type-Theoretic Considerations
• Logical relations for monadic types
• scientific article; zbMATH DE number 512954 (Why is no real title available?)
• scientific article; zbMATH DE number 1948186 (Why is no real title available?)
• Type theory based on dependent inductive and coinductive types
• Monotone (co)inductive types and positive fixed-point types
• scientific article; zbMATH DE number 1434122 (Why is no real title available?)
• Programming Languages and Systems
• Equational theories for inductive types
• Paradoxical connectives: proof-theoretic semantics, recursion, and fixed-point operators
• On the internal structures of inductive types

This page was built for publication: Logical relations and inductive/coinductive types

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