Typed -calculus with recursive definitions

DOI10.1007/BFB0023879MaRDI QIDQ2757815zbMATH OpenOpenAlexFDO

Authors S. V. Kotov

Publication date 4 December 2001

Published in Logical Foundations of Computer Science — Tver '92 (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• Structural recursive definitions in type theory
• General recursive functions in a very simply interpretable typed -calculus
• Type-based termination of recursive definitions
• Non-standard reductions and categorical models in typed lambda-calculus
• scientific article; zbMATH DE number 4047683

Cited in

(23)

• General recursive functions in a very simply interpretable typed -calculus
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• A term calculus for (co-)recursive definitions on streamlike data structures
• Recursion over objects of functional type
• Typed operational semantics
• Untyped -calculus with relative typing
• Typed ψ-calculi
• scientific article; zbMATH DE number 445155 (Why is no real title available?)
• scientific article; zbMATH DE number 3854393 (Why is no real title available?)
• scientific article; zbMATH DE number 3954870 (Why is no real title available?)
• scientific article; zbMATH DE number 3980461 (Why is no real title available?)
• scientific article; zbMATH DE number 4047683 (Why is no real title available?)
• scientific article; zbMATH DE number 4050954 (Why is no real title available?)
• A game-theoretic, concurrent and fair model of the typed -calculus, with full recursion
• Structural recursive definitions in type theory
• Explicitly typed -calculus for polymorphism and call-by-value
• scientific article; zbMATH DE number 512879 (Why is no real title available?)
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
• Gamma-reduction in type theory of acyclic recursion
• Non-standard reductions and categorical models in typed lambda-calculus
• Recursive function definition for types with binders
• A user's friendly syntax to define recursive functions as typed λ-terms
• Partial inductive definitions as type-systems for \(\lambda\)-terms

This page was built for publication: Typed \(\lambda\)-calculus with recursive definitions

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