Intuitionistic fixed point logic
From MaRDI portal
Computation over the reals, computable analysis (03D78) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Continuous lattices and posets, applications (06B35) Constructive and recursive analysis (03F60) Inductive definability (03D70)
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
- 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?)
- 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
- 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
- \textsc{Prawf}: an interactive proof system for program extraction
Cited in
(20)- Type-theoretic approaches to ordinals
- \textsc{Prawf}: an interactive proof system for program extraction
- scientific article; zbMATH DE number 749933 (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
- scientific article; zbMATH DE number 1870424 (Why is no real title available?)
- Least and greatest fixed points in intuitionistic natural deduction
- Extracting total Amb programs from proofs
- scientific article; zbMATH DE number 6680142 (Why is no real title available?)
- Explicit fixed points in interpretability logic
- Extracting non-deterministic concurrent programs
- Intuitionistic ancestral logic
- Fixed-Point Elimination in the Intuitionistic Propositional Calculus
- Computing with continuous objects: a uniform co-inductive approach
- Computational expressivity of (circular) proofs with fixed points
- Intuitionistic Trilattice Logics
- Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
- Extracting efficient exact real number computation from proofs in constructive type theory
- scientific article; zbMATH DE number 7731929 (Why is no real title available?)
- An intuitionistic fixed point theory
- The compatibility of the minimalist foundation with homotopy 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)
