Switch to: References

Citations of:

On the correspondence between proofs and lamba-terms

In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia (1995)

Add citations

You must login to add citations.
  1. Lambda Calculus and Intuitionistic Linear Logic.Simona Ronchi Della Rocca & Luca Roversi - 1997 - Studia Logica 59 (3):417-448.
    The introduction of Linear Logic extends the Curry-Howard Isomorphism to intensional aspects of the typed functional programming. In particular, every formula of Linear Logic tells whether the term it is a type for, can be either erased/duplicated or not, during a computation. So, Linear Logic can be seen as a model of a computational environment with an explicit control about the management of resources.
    Download  
     
    Export citation  
     
    Bookmark  
  • Relational nouns, pronouns, and resumption.Ash Asudeh - 2005 - Linguistics and Philosophy 28 (4):375 - 446.
    This paper presents a variable-free analysis of relational nouns in Glue Semantics, within a Lexical Functional Grammar (LFG) architecture. Relational nouns and resumptive pronouns are bound using the usual binding mechanisms of LFG. Special attention is paid to the bound readings of relational nouns, how these interact with genitives and obliques, and their behaviour with respect to scope, crossover and reconstruction. I consider a puzzle that arises regarding relational nouns and resumptive pronouns, given that relational nouns can have bound readings (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Typing untyped λ-terms, or reducibility strikes again!Jean Gallier - 1998 - Annals of Pure and Applied Logic 91 (2-3):231-270.
    It was observed by Curry that when λ-terms can be assigned types, for example, simple types, these terms have nice properties . Coppo, Dezani, and Veneri, introduced type systems using conjunctive types, and showed that several important classes of terms can be characterized according to the shape of the types that can be assigned to these terms. For example, the strongly normalizable terms, the normalizable terms, and the terms having head-normal forms, can be characterized in some systems and Ω. The (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation