Intuitionistic fixed point logic
From MaRDI portal
Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Inductive definability (03D70) Computation over the reals, computable analysis (03D78) Constructive and recursive analysis (03F60) Continuous lattices and posets, applications (06B35)
Abstract: We study the system IFP of intuitionistic fixed point logic, an extension of intuitionistic first-order logic by strictly positive inductive and coinductive definitions. We define a realizability interpretation of IFP and use it to extract computational content from proofs about abstract structures specified by arbitrary classically true disjunction free formulas. The interpretation is shown to be sound with respect to a domain-theoretic denotational semantics and a corresponding lazy operational semantics of a functional language for extracted programs. We also show how extracted programs can be translated into Haskell. As an application we extract a program converting the signed digit representation of real numbers to infinite Gray-code from a proof of inclusion of the corresponding coinductive predicates.
Recommendations
Cites work
- \textsc{Prawf}: an interactive proof system for program extraction
- A coinductive approach to computing with compact sets
- A syntactic view of computational adequacy
- Algebraic semantics for coalgebraic logics
- An abstract data type for real numbers
- An ideal model for recursive polymorphic types
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Canonical effective subalgebras of classical algebras as constructive metric completions
- Computational adequacy for recursive types in models of intuitionistic set theory
- Constructivism in mathematics. An introduction. Volume II
- Continuous Lattices and Domains
- Copatterns, programming infinite structures by observations
- Dependent choice, `quote' and the clock
- Extracting non-deterministic concurrent programs
- From Coinductive Proofs to Exact Real Arithmetic
- From coinductive proofs to exact real arithmetic: theory and applications
- Functional interpretation and inductive definitions
- General logical metatheorems for functional analysis
- Handbook of modal logic
- scientific article; zbMATH DE number 1705158 (Why is no real title available?)
- scientific article; zbMATH DE number 439891 (Why is no real title available?)
- scientific article; zbMATH DE number 5360217 (Why is no real title available?)
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 4070894 (Why is no real title available?)
- scientific article; zbMATH DE number 3687373 (Why is no real title available?)
- scientific article; zbMATH DE number 3780545 (Why is no real title available?)
- scientific article; zbMATH DE number 1064116 (Why is no real title available?)
- scientific article; zbMATH DE number 2003148 (Why is no real title available?)
- scientific article; zbMATH DE number 1460545 (Why is no real title available?)
- scientific article; zbMATH DE number 949290 (Why is no real title available?)
- scientific article; zbMATH DE number 1841846 (Why is no real title available?)
- scientific article; zbMATH DE number 783754 (Why is no real title available?)
- scientific article; zbMATH DE number 3216998 (Why is no real title available?)
- scientific article; zbMATH DE number 3291134 (Why is no real title available?)
- scientific article; zbMATH DE number 2247249 (Why is no real title available?)
- scientific article; zbMATH DE number 2247254 (Why is no real title available?)
- Induction-recursion and initial algebras.
- Inductive types and type constraints in the second-order lambda calculus
- Inductive-inductive definitions
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- LCF considered as a programming language
- Logic for Gray-code computation
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Minlog -- a tool for program extraction supporting algebras and coalgebras
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
- On the interpretation of intuitionistic number theory
- On the intuitionistic strength of monotone inductive definitions
- On the proof-theoretic strength of monotone induction in explicit mathematics
- Optimized program extraction for induction and coinduction
- PCF extended with real numbers
- Proofs and computations
- Proofs, programs, processes
- Ramified Corecurrence and Logspace
- Real number computation through Gray code embedding.
- Real number computation with committed choice logic programming languages
- Realisability for induction and coinduction with applications to constructive analysis
- Results on the propositional \(\mu\)-calculus
- Set-theoretical and other elementary models of the \(\lambda\)-calculus
- Some logical metatheorems with applications in functional analysis
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory
- Undecidability of equality for codata types
- Weighted relational models of typed lambda-calculi
Cited in
(20)- Explicit fixed points in interpretability logic
- An intuitionistic fixed point theory
- \textsc{Prawf}: an interactive proof system for program extraction
- Type-theoretic approaches to ordinals
- Fixed-Point Elimination in the Intuitionistic Propositional Calculus
- scientific article; zbMATH DE number 6680142 (Why is no real title available?)
- Intuitionistic Trilattice Logics
- scientific article; zbMATH DE number 749933 (Why is no real title available?)
- scientific article; zbMATH DE number 1870424 (Why is no real title available?)
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- Computing with continuous objects: a uniform co-inductive approach
- Intuitionistic ancestral logic
- Extracting non-deterministic concurrent programs
- Least and greatest fixed points in intuitionistic natural deduction
- The compatibility of the minimalist foundation with homotopy type theory
- scientific article; zbMATH DE number 7731929 (Why is no real title available?)
- Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
- Extracting total Amb programs from proofs
- Computational expressivity of (circular) proofs with fixed points
- Extracting efficient exact real number computation from proofs in constructive type theory
This page was built for publication: Intuitionistic fixed point logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2220485)
