Partial proof terms in the study of idealized proof search
From MaRDI portal
Publication:6648177
DOI10.1007/978-3-031-66997-2_16MaRDI QIDQ6648177
José Espírito Santo, Ana Catarina Sousa
Publication date: 4 December 2024
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The \(\lambda \)-calculus and the unity of structural proof theory
- Lectures on the Curry-Howard isomorphism
- Focusing and polarization in linear, intuitionistic, and classical logics
- Normal natural deduction proofs (in classical logic)
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
- The polarized \(\lambda\)-calculus
- Normal proofs and their grammar
- Towards a canonical classical natural deduction system
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
- A coinductive approach to proof search through typed lambda-calculi
- A short note on type-inhabitation: formula-trees vs. game semantics
- Uniform proofs as a foundation for logic programming
- Dependent types and explicit substitutions: A meta-theoretical development
- Game Semantics and Uniqueness of Type Inhabitance in the Simply-Typed λ-Calculus
- A Linear Spine Calculus
- Decidability of Several Concepts of Finiteness for Simple Types
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- Contextual modal type theory
- Automata Theoretic Account of Proof Search
- Mechanizing Mathematical Reasoning
- Logical Approaches to Computational Barriers
- Proof-term synthesis on dependent-type systems via explicit substitutions
This page was built for publication: Partial proof terms in the study of idealized proof search
