scientific article; zbMATH DE number 2185726

MaRDI QIDQ3024919zbMATH OpenFDO

Authors Paweł Urzyczyn

Publication date 4 July 2005

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Complexity of computation (including implicit computational complexity) (03D15) Undecidability and degrees of sets of sentences (03D35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Recommendations

• Inhabitation of types in the simply typed lambda calculus
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• scientific article; zbMATH DE number 3902021
• scientific article; zbMATH DE number 1499090
• Type checking and typability in domain-free lambda calculi
• Term-space semantics of typed lambda calculus
• Realizing the dependently typed -calculus
• The complexity of type inference for higher-order typed lambda calculi
• Semantics of a typed algebraic lambda-calculus
• scientific article; zbMATH DE number 4037857

Cited in

(24)

• Type reconstruction in finite rank fragments of the second-order -calculus
• Infiniteness of \(\text{proof}(\alpha)\) is polynomial-space complete
• Inhabitation of types in the simply typed lambda calculus
• Normal proofs and their grammar
• A short note on type-inhabitation: formula-trees vs. game semantics
• A simple proof of the undecidability of inhabitation in λP
• scientific article; zbMATH DE number 3854393 (Why is no real title available?)
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Inhabitation for non-idempotent intersection types
• scientific article; zbMATH DE number 2085249 (Why is no real title available?)
• Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
• Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic
• A unifying framework for type inhabitation
• Practical Proof Search for Coq by Type Inhabitation
• A simpler undecidability proof for system F inhabitation
• scientific article; zbMATH DE number 7204434 (Why is no real title available?)
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• Realist consequence, epistemic inference, computational correctness
• A partial translation from \({\lambda}U\) to \({\lambda}2\)
• Solvability = typability + inhabitation
• The existential fragment of second-order propositional intuitionistic logic is undecidable
• Inhabitation of polymorphic and existential types
• Type checking and typability in domain-free lambda calculi
• Pregrammars and intersection types

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3024919)