Computation by infinite descent made explicit
From MaRDI portal
Cites work
- -Calculus with Explicit Points and Approximations
- A lattice-theoretical fixpoint theorem and its applications
- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
- Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs
- Categorical logic and type theory
- Circular proofs for the Gödel-Löb provability logic
- Classical system of Martin-Löf's inductive definitions is not equivalent to cyclic proofs
- Completeness of Kozen's axiomatisation of the propositional \(\mu\)-calculus.
- Computational expressivity of (circular) proofs with fixed points
- Cyclic arithmetic is equivalent to Peano arithmetic
- Cyclic proofs for the first-order -calculus
- Equivalence of inductive definitions and cyclic proofs under arithmetic
- Games for the -calculus
- scientific article; zbMATH DE number 6680140 (Why is no real title available?)
- scientific article; zbMATH DE number 1956528 (Why is no real title available?)
- scientific article; zbMATH DE number 2087442 (Why is no real title available?)
- scientific article; zbMATH DE number 7155168 (Why is no real title available?)
- Infinitary proof theory: the multiplicative additive case
- Least and greatest fixed points in linear logic
- Least and Greatest Fixpoints in Game Semantics
- Lectures on the Curry-Howard isomorphism
- NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC
- On global induction mechanisms in aμ-calculus with explicit approximations
- Practical coinduction
- Results on the propositional \(\mu\)-calculus
- Sequent calculi for induction and infinite descent
- Un théorème sur les fonctions d'ensembles.
- Wellfounded recursion with copatterns: a unified approach to termination and productivity
This page was built for publication: Computation by infinite descent made explicit
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7308608)