Existential Type Systems with No Types in Terms

DOI10.1007/978-3-642-02273-9_10zbMath1246.03028OpenAlexW1576139432MaRDI QIDQ3637189

Aleksy Schubert, Ken-etsu Fujita

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_10

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Related Items

Existential type systems between Church and Curry style (type-free style) ⋮ The existential fragment of second-order propositional intuitionistic logic is undecidable ⋮ Type checking and typability in domain-free lambda calculi ⋮ The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types ⋮ A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments

Uses Software

• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Lectures on the Curry-Howard isomorphism
• CPS-translation as adjoint
• The undecidability of the semi-unification problem
• Typability and type checking in System F are equivalent and undecidable
• Constructive proofs of the range property in lambda calculus
• A normalization-procedure for the first order classical natural deduction with full logical symbols
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Domain-free pure type systems
• Typed Lambda Calculi and Applications