Dual Calculus with Inductive and Coinductive Types

DOI10.1007/978-3-642-02348-4_16MaRDI QIDQ3636828zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Automated Reasoning with Analytic Tableaux and Related Methods
• Call-by-value and call-by-name dual calculi with inductive and coinductive types
• Type theory based on dependent inductive and coinductive types
• Dualized simple type theory
• scientific article; zbMATH DE number 2061701
• scientific article; zbMATH DE number 2182487
• Inductively defined types in the Calculus of Constructions
• Mixed Inductive/Coinductive Types and Strong Normalization
• scientific article; zbMATH DE number 7699441
• Realization of coinductive types

Cites work

• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1948183 (Why is no real title available?)
• scientific article; zbMATH DE number 2080223 (Why is no real title available?)
• A symmetric lambda calculus for classical program extraction
• Call-by-Value Is Dual to Call-by-Name, Extended
• Call-by-value is dual to call-by-name
• Control categories and duality: On the categorical semantics of the lambda-mu calculus
• Inductive types and type constraints in the second-order lambda calculus
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Proofs of strong normalisation for second order classical natural deduction
• Realizability interpretation of coinductive definitions and program synthesis with streams
• Term Rewriting and Applications
• The duality of computation
• Types for Proofs and Programs

Cited in

(6)

• Classical logic with Mendler induction
• Strong Normalization and Equi-(Co)Inductive Types
• Dualized simple type theory
• Classical Logic with Mendler Induction
• Type theory based on dependent inductive and coinductive types
• Call-by-value and call-by-name dual calculi with inductive and coinductive types

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

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