Dual Calculus with Inductive and Coinductive Types

DOI10.1007/978-3-642-02348-4_16zbMath1242.03085OpenAlexW1744323313MaRDI QIDQ3636828

Daisuke Kimura, Makoto Tatsuta

Publication date: 30 June 2009

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02348-4_16

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Classical Logic with Mendler Induction ⋮ Dualized Simple Type Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Realizability interpretation of coinductive definitions and program synthesis with streams
• A symmetric lambda calculus for classical program extraction
• Inductive types and type constraints in the second-order lambda calculus
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• The duality of computation
• Call-by-Value Is Dual to Call-by-Name, Extended
• Proofs of strong normalisation for second order classical natural deduction
• Call-by-value is dual to call-by-name
• Term Rewriting and Applications
• Types for Proofs and Programs

This page was built for publication: Dual Calculus with Inductive and Coinductive Types