Non-idempotent intersection types for the Lambda-Calculus

, &
Logic Journal of the IGPL 25 (4):431-464 (2017)
  Copy   BIBTEX

Abstract

This article has no associated abstract. (fix it)

Categories

Keywords

Reprint years

DOI

10.1093/jigpal/jzx018

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

An elementary proof of strong normalization for intersection types.Valentini Silvio - 2001 - Archive for Mathematical Logic 40 (7):475-488.
Intersection types for lambda-terms and combinators and their logics.Martin Bunder - 2002 - Logic Journal of the IGPL 10 (4):357-378.
Intersection Type Systems and Logics Related to the Meyer–Routley System B+.Martin Bunder - 2003 - Australasian Journal of Logic 1:43-55.
Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.
Cut-Elimination in the Strict Intersection Type Assignment System is Strongly Normalizing.Steffen van Bakel - 2004 - Notre Dame Journal of Formal Logic 45 (1):35-63.
Lambda calculus with types.H. P. Barendregt - 2013 - New York: Cambridge University Press. Edited by Wil Dekkers & Richard Statman.
Strong Normalization and Typability with Intersection Types.Silvia Ghilezan - 1996 - Notre Dame Journal of Formal Logic 37 (1):44-52.
Unification in a A-Calculus with Intersection Types.Michael Kohlhase & Frank Pfenning - unknown
Variable-free formalization of the Curry-Howard theory.William Tait - manuscript
Inductive types and type constraints in the second-order lambda calculus.Nax Paul Mendler - 1991 - Annals of Pure and Applied Logic 51 (1-2):159-172.
$lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
Lambda Calculi: A Guide for the Perplexed.Chris Hankin - 1994 - Oxford University Press.
The lambda calculus: its syntax and semantics.Hendrik Pieter Barendregt - 1981 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co..
Recursion theory and the lambda-calculus.Robert E. Byerly - 1982 - Journal of Symbolic Logic 47 (1):67-83.
Making the Hyperreal Line Both Saturated and Complete.H. Jerome Keisler & James H. Schmerl - 1991 - Journal of Symbolic Logic 56 (3):1016-1025.

Analytics

Added to PP
2019-01-10

Downloads
13 (#1,006,512)

6 months
5 (#652,053)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Linear Logic.Jean-Yves Girard - 1987 - Theoretical Computer Science 50:1–102.
Intensional interpretations of functionals of finite type I.W. W. Tait - 1967 - Journal of Symbolic Logic 32 (2):198-212.
Combinatory Logic, Volume I.Haskell B. Curry, Robert Feys & William Craig - 1959 - Philosophical Review 68 (4):548-550.
Lambda calculus with types.H. P. Barendregt - 2013 - New York: Cambridge University Press. Edited by Wil Dekkers & Richard Statman.

View all 15 references / Add more references