Intuitionistic fixed point logic
From MaRDI portal
Publication:2220485
DOI10.1016/j.apal.2020.102903zbMath1498.03065arXiv2002.00188OpenAlexW3092637222MaRDI QIDQ2220485
Publication date: 25 January 2021
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2002.00188
Constructive and recursive analysis (03F60) Logic in computer science (03B70) Continuous lattices and posets, applications (06B35) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Inductive definability (03D70) Computation over the reals, computable analysis (03D78)
Related Items (8)
Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ 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 ⋮ Type-theoretic approaches to ordinals ⋮ Unnamed Item ⋮ Computing with continuous objects: a uniform co-inductive approach ⋮ \textsc{Prawf}: an interactive proof system for program extraction
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Proofs, programs, processes
- Results on the propositional \(\mu\)-calculus
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Constructivism in mathematics. An introduction. Volume II
- New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic
- LCF considered as a programming language
- Set-theoretical and other elementary models of the \(\lambda\)-calculus
- PCF extended with real numbers
- On the proof-theoretic strength of monotone induction in explicit mathematics
- Induction-recursion and initial algebras.
- Real number computation through Gray code embedding.
- A syntactic view of computational adequacy
- Optimized program extraction for induction and coinduction
- Real number computation with committed choice logic programming languages
- Undecidability of equality for codata types
- Dependent choice, `quote' and the clock
- Computational adequacy for recursive types in models of intuitionistic set theory
- An abstract data type for real numbers
- \textsc{Prawf}: an interactive proof system for program extraction
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Inductive types and type constraints in the second-order lambda calculus
- Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions
- Copatterns
- A coinductive approach to computing with compact sets
- From coinductive proofs to exact real arithmetic: theory and applications
- Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras
- Proofs and Computations
- Inductive-Inductive Definitions
- From Coinductive Proofs to Exact Real Arithmetic
- Functional interpretation and inductive definitions
- An ideal model for recursive polymorphic types
- Continuous Lattices and Domains
- Some logical metatheorems with applications in functional analysis
- Logic for Gray-code Computation
- Weighted Relational Models of Typed Lambda-Calculi
- Extracting Non-Deterministic Concurrent Programs.
- On the intuitionistic strength of monotone inductive definitions
- General logical metatheorems for functional analysis
- Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
- Ramified Corecurrence and Logspace
- On the interpretation of intuitionistic number theory
- Typed lambda-calculus in classical Zermelo-Fraenkel set theory
This page was built for publication: Intuitionistic fixed point logic
