Least and greatest fixed points in intuitionistic natural deduction
From MaRDI portal
Publication:5958300
DOI10.1016/S0304-3975(00)00355-8zbMath0984.68136OpenAlexW1992801334WikidataQ62043281 ScholiaQ62043281MaRDI QIDQ5958300
Publication date: 3 March 2002
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0304-3975(00)00355-8
natural deduction(co)inductive typescoding stylesleast and greatest fixed pointsschemes of (total) (co)recursiontyped lambda calculi
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Some Remarks on Type Systems for Course-of-value Recursion ⋮ An induction principle for nested datatypes in intensional type theory ⋮ Two extensions of system F with (co)iteration and primitive (co)recursion principles
Uses Software
Cites Work
- Data structures and program transformation
- Automatic synthesis of typed \(\Lambda\)-programs on term algebras
- Recursive programming with proofs
- The extended calculus of constructions (ECC) with inductive types
- Paramorphisms
- Inductive types and type constraints in the second-order lambda calculus
- A lattice-theoretical fixpoint theorem and its applications
- Type fixpoints
- Positive recursive type assignment
- A natural extension of natural deduction
- A framework for defining logics
- Inductively defined types in the Calculus of Constructions
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Least and greatest fixed points in intuitionistic natural deduction
