Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (1)

A coinductive approach to proof search through typed lambda-calculi

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