Realisability and adequacy for (co)induction
From MaRDI portal
Recommendations
- Realisability for induction and coinduction with applications to constructive analysis
- From realizability to induction via dependent intersection
- Logical Approaches to Computational Barriers
- Realizability interpretation of generalized inductive definitions
- Realizability interpretation of proofs in constructive analysis
- Induction, coinduction, and adjoints
- Coinductive Formal Reasoning in Exact Real Arithmetic
- From Coinductive Proofs to Exact Real Arithmetic
- Realizability and intuitionistic logic
- scientific article; zbMATH DE number 1696612
Cited in
(13)- Recursion over realizability structures
- Optimized program extraction for induction and coinduction
- Induction, coinduction, and adjoints
- Global semantic typing for inductive and coinductive computing
- Global semantic typing for inductive and coinductive computing
- Realisability for induction and coinduction with applications to constructive analysis
- Program extraction via typed realisability for induction and coinduction
- Proofs, programs, processes
- TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS
- A realizability interpretation of Church's simple theory of types
- Nonflatness and totality
- A coinductive semantics of the unlimited register machine
- Internalising modified realisability in constructive type theory
This page was built for publication: Realisability and adequacy for (co)induction
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2917339)
