Existential type systems between Church and Curry style (type-free style)
From MaRDI portal
Publication:402117
DOI10.1016/j.tcs.2014.05.019zbMath1393.03004MaRDI QIDQ402117
Ken-etsu Fujita, Aleksy Schubert
Publication date: 27 August 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2014.05.019
undecidability; typability; type checking; Church-style type system; existential types; type-free type system
03B40: Combinatory logic and lambda calculus
Related Items
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The undecidability of type related problems in the type-free style System F with finitely stratified polymorphic types
- Lectures on the Curry-Howard isomorphism
- CPS-translation as adjoint
- Finitely stratified polymorphism
- Typability and type checking in System F are equivalent and undecidable
- The undecidability of the second order predicate unification problem
- Domain-Freeλµ-Calculus
- Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence
- Existential Type Systems with No Types in Terms
- Embedding first order predicate logic in fragments of intuitionistic logic
- Domain-free pure type systems
- Unification of higher-order patterns in linear time and space
- A logic programming language with lambda-abstraction, function variables, and simple unification
- Complete and easy bidirectional typechecking for higher-rank polymorphism
- Relational Parametricity and Control
- THE UNDECIDABILITY OF TYPE RELATED PROBLEMS IN TYPE -FREE STYLE SYSTEM F
- The Principal Type-Scheme of an Object in Combinatory Logic
- Typed Lambda Calculi and Applications
- Types for Proofs and Programs
