Type checking and typability in domain-free lambda calculi

DOI10.1016/j.tcs.2011.06.020zbMath1241.03011OpenAlexW2150562546MaRDI QIDQ655411

Hiroshi Nakano, Makoto Tatsuta, Yukiyoshi Kameyama, Koji Nakazawa

Publication date: 4 January 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.06.020

zbMATH Keywords

undecidabilitytypabilitytype checkingexistential typeCPS translationdomain-free type system

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• A syntactic embedding of predicate logic into second-order propositional logic
• Inhabitation of polymorphic and existential types
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Typability and type checking in System F are equivalent and undecidable
• Natural deduction with general elimination rules
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Existential Type Systems with No Types in Terms
• Representing Control: a Study of the CPS Transformation
• Domain-free pure type systems
• Relational Parametricity and Control
• Typed Lambda Calculi and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Type checking and typability in domain-free lambda calculi