A coinductive approach to proof search through typed lambda-calculi
From MaRDI portal
Publication:2231698
DOI10.1016/J.APAL.2021.103026OpenAlexW2491817307MaRDI QIDQ2231698
Ralph Matthes, José Espírito Santo, Luís Pinto
Publication date: 30 September 2021
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1602.04382
Functional programming and lambda calculus (68N18) Structure of proofs (03F07) Combinatory logic and lambda calculus (03B40)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Lectures on the Curry-Howard isomorphism
- Counting proofs in propositional logic
- Focusing and polarization in linear, intuitionistic, and classical logics
- The polarized \(\lambda\)-calculus
- Normal proofs and their grammar
- A short note on type-inhabitation: formula-trees vs. game semantics
- Operational semantics of resolution and productivity in Horn clause logic
- Uniform proofs as a foundation for logic programming
- Proof Relevant Corecursive Resolution
- Permutations in Coinductive Graph Representation
- Coalgebraic Derivations in Logic Programming
- Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus
- On Long Normal Inhabitants of a Type
- The Inhabitation Problem for Non-idempotent Intersection Types
- Two loop detection mechanisms: A comparison
- The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
- Decidability of Several Concepts of Finiteness for Simple Types
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- Automata Theoretic Account of Proof Search
- Intersection type calculi of bounded dimension
- Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis
This page was built for publication: A coinductive approach to proof search through typed lambda-calculi
