Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
From MaRDI portal
Publication:5236550
DOI10.1017/S0960129518000099zbMath1456.03024arXiv1604.02086OpenAlexW2964018350MaRDI QIDQ5236550
Ralph Matthes, José Espírito Santo, Luís Pinto
Publication date: 9 October 2019
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1604.02086
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Counting proofs in propositional logic
- Focusing and polarization in linear, intuitionistic, and classical logics
- Normal proofs and their grammar
- A short note on type-inhabitation: formula-trees vs. game semantics
- Programming with Higher-Order Logic
- 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
- 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: Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
