Type checking and typability in domain-free lambda calculi

DOI10.1016/J.TCS.2011.06.020MaRDI QIDQ655411zbMATH OpenOpenAlexFDO

Authors Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano

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

CPS translationdomain-free type systemexistential typetypabilitytype checkingundecidability

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Typability and type checking in System F are equivalent and undecidable
• scientific article; zbMATH DE number 2185726
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems

Cites work

• A syntactic embedding of predicate logic into second-order propositional logic
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Domain-free pure type systems
• Existential Type Systems with No Types in Terms
• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 3485174 (Why is no real title available?)
• scientific article; zbMATH DE number 1324438 (Why is no real title available?)
• scientific article; zbMATH DE number 1342279 (Why is no real title available?)
• scientific article; zbMATH DE number 1759491 (Why is no real title available?)
• Inhabitation of polymorphic and existential types
• Natural deduction with general elimination rules
• Relational Parametricity and Control
• Representing Control: a Study of the CPS Transformation
• Typability and type checking in System F are equivalent and undecidable
• Typed Lambda Calculi and Applications

Cited in

(7)

• Typability and type checking in System F are equivalent and undecidable
• scientific article; zbMATH DE number 2185726 (Why is no real title available?)
• Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
• Type Checking and Inference Are Equivalent in Lambda Calculi with Existential Types
• Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
• Type checking and inference for polymorphic and existential types in multiple-quantifier and type-free systems
• Checking Emptiness of Non-Deterministic Regular Types with Set Operators

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

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