Author | Title | Year | Journal/Proceedings | BibTeX type | DOI/URL |
---|---|---|---|---|---|

Alves, S. & Florido, Má. | Weak linearization of the lambda calculus [BibTeX] |
2005 | Theoretical Computer Science Vol. 342(1), pp. 79-103 |
article | URL |

BibTeX:
@article{SAMF:05, author = {Sandra Alves and Mário Florido}, title = {Weak linearization of the lambda calculus}, journal = {Theoretical Computer Science}, year = {2005}, volume = {342}, number = {1}, pages = {79--103}, url = {http://dx.doi.org/10.1016/j.tcs.2005.06.005} } |
|||||

Barbanera, F. & Berardi, S. | A Symmetric Lambda Calculus for Classical Program Extraction [BibTeX] |
1996 | Information and Compution Vol. 125(2), pp. 103-117 |
article | |

BibTeX:
@article{FBSB:96, author = {Franco Barbanera and Stefano Berardi}, title = {A Symmetric Lambda Calculus for Classical Program Extraction}, journal = {Information and Compution}, year = {1996}, volume = {125}, number = {2}, pages = {103--117} } |
|||||

Barendregt, H. | The Impact of the Lambda Calculus on Logic and Computer Science [BibTeX] |
1997 | Bulletin of Symbolic Logic Vol. 3(3), pp. 181-215 |
article | URL |

BibTeX:
@article{HB:97, author = {Henk Barendregt}, title = {The Impact of the Lambda Calculus on Logic and Computer Science}, journal = {Bulletin of Symbolic Logic}, year = {1997}, volume = {3}, number = {3}, pages = {181--215}, url = {ftp://math.ucla.edu/pub/asl/bsl/0302/0302-003.ps} } |
|||||

Barendregt, H.P. | Lambda Calculi with Types [BibTeX] |
1991 | Vol. 2Handbook of Logic in Computer Science |
incollection | URL |

BibTeX:
@incollection{Bar:93, author = {H. P. Barendregt}, title = {Lambda Calculi with Types}, booktitle = {Handbook of Logic in Computer Science}, publisher = {Oxford University Press}, year = {1991}, volume = {2}, note = {http://citeseer.ist.psu.edu/barendregt92lambda.htmlElectronic Edition}, url = {http://citeseer.ist.psu.edu/barendregt92lambda.html and http://www.cs.ru.nl/~henk/Personal Webpage} } |
|||||

Barendregt, H.P. | The Lambda Calculus Its Syntax and Semantics [BibTeX] |
1984 | Vol. 103 |
book | |

BibTeX:
@book{Bar:84, author = {H. P. Barendregt}, title = {The Lambda Calculus Its Syntax and Semantics}, publisher = {North Holland}, year = {1984}, volume = {103}, edition = {Revised}, note = {http://www.cs.ru.nl/~henk/Personal Webpage} } |
|||||

Bergstra & Klop | Invertible Terms in the Lambda Calculus [BibTeX] |
1980 | Theoretical Computer Science Vol. 11, pp. 19 - 37 |
article | |

BibTeX:
@article{JBJK:80, author = {Bergstra and Klop}, title = {Invertible Terms in the Lambda Calculus}, journal = {Theoretical Computer Science}, year = {1980}, volume = {11}, pages = {19 -- 37} } |
|||||

Bierman, G.M. | A Classical Linear lambda-calculus [BibTeX] |
1999 | Theoretical Computer Science Vol. 227(1-2), pp. 43-78 |
article | DOI |

BibTeX:
@article{Bie:97, author = {G. M. Bierman}, title = {A Classical Linear lambda-calculus}, journal = {Theoretical Computer Science}, year = {1999}, volume = {227}, number = {1-2}, pages = {43-78}, note = {http://dx.doi.org/10.1016/S0304-3975(99)00048-1Electronic Edition}, doi = {http://dx.doi.org/10.1016/S0304-3975(99)00048-1} } |
|||||

Blanqui, F., Jouannaud, J. & Okada, M. | Inductive-data-type Systems | 2002 | Theoretical Computer Science Vol. 272, pp. 41 - 68 |
article | URL |

Abstract: In a previous work (``Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed lambda-calculus enriched by pattern-matching definitions following a certain format, called the ``General Schema'', which generalizes the usual recursor definitions for natural numbers and similar ``basic inductive types''. This combined language was shown to be strongly normalizing. The purpose of this paper is to reformulate and extend the General Schema in order to make it easily extensible, to capture a more general class of inductive types, called ``strictly positive'', and to ease the strong normalization proof of the resulting system. This result provides a computation model for the combination of an algebraic specification language based on abstract data types and of a strongly typed functional language with strictly positive inductive types. |
|||||

BibTeX:
@article{FBJJMO:08, author = {Frédéric Blanqui and Jean-Pierre Jouannaud and Mitsuhiro Okada}, title = {Inductive-data-type Systems}, journal = {Theoretical Computer Science}, publisher = {HAL - CCSD}, year = {2002}, volume = {272}, pages = {41 -- 68}, url = {http://hal.inria.fr/inria-00105578/en} } |
|||||

de Bruijn, N.G. | Lambda Calculus Notation with Nameless Dummies, A Tool for Automatic Formula Manipulation, With Applications to the Church-Rosser Theorem [BibTeX] |
1972 | Indagationes Mathematicae (Koninglijke Nederlandse Akademie van Wetenschappen) Vol. 34(5), pp. 381-392 |
article | |

BibTeX:
@article{dB:72, author = {N. G. de Bruijn}, title = {Lambda Calculus Notation with Nameless Dummies, A Tool for Automatic Formula Manipulation, With Applications to the Church-Rosser Theorem}, journal = {Indagationes Mathematicae (Koninglijke Nederlandse Akademie van Wetenschappen)}, year = {1972}, volume = {34}, number = {5}, pages = {381--392}, note = {http://www.win.tue.nl/automath/archive/pdf/aut029.pdfElectronic Edition} } |
|||||

Considine, J. | Deciding Isomorphisms of Simple Types in Polynomial Time | 2000 | (2000-010) | techreport | URL |

Abstract: The isomorphisms holding in all models of the simply typed lambda calculus with surjective and terminal objects are well studied - these models are exactly the Cartesian closed categories. Isomorphism of two simple types in such a model is decidable by reduction to a normal form and comparison under a finite number of permutations (Bruce, Di Cosmo, and Longo 1992). Unfortunately, these normal forms may be exponentially larger than the original types so this construction decides isomorphism in exponential time. We show how using space-sharing/hash-consing techniques and memoization can be used to decide isomorphism in practical polynomial time (low degree, small hidden constant). Other researchers have investigated simple type isomorphism in relation to, among other potential applications, type-based retrieval of software modules from libraries and automatic generation of bridge code for multi-language systems. Our result makes such potential applications practically feasible. |
|||||

BibTeX:
@techreport{JC:00b, author = {Jeffrey Considine}, title = {Deciding Isomorphisms of Simple Types in Polynomial Time}, year = {2000}, number = {2000-010}, note = {Wed, 22 Oct 2008 14:29:30 GMT}, url = {http://www.cs.bu.edu/techreports/2000-010-deciding-simple-type-isomorphisms.ps.Z} } |
|||||

Cosmo, R.D. | Isomorphisms of Types: from Lambda-calculus to information retrieval and languages design [BibTeX] |
1995 | book | ||

BibTeX:
@book{DC:95, author = {R. Di Cosmo}, title = {Isomorphisms of Types: from Lambda-calculus to information retrieval and languages design}, publisher = {Birkhaeuser}, year = {1995}, note = {http://books.google.com/books?id=cdJZRjIxavwC&dq=Isomorphisms+of+Types:+from+Lambda-calculus+to+information+retrieval+and+languages+design&source=gbs_summary_s&cad=0Electronic Edition} } |
|||||

Cosmo, R.D. | Second Order Isomorphic Types: A Proof Theoretic Study on Second Order lambda-Calculus with Surjective Paring and Terminal Object [BibTeX] |
1995 | Information and Compution Vol. 119(2), pp. 176-201 |
article | |

BibTeX:
@article{DiC:95, author = {Roberto Di Cosmo}, title = {Second Order Isomorphic Types: A Proof Theoretic Study on Second Order lambda-Calculus with Surjective Paring and Terminal Object}, journal = {Information and Compution}, year = {1995}, volume = {119}, number = {2}, pages = {176-201} } |
|||||

Dezani-Ciancaglini, M. | Characterization of Normal Forms Possesing Inverse in the $beta eta$-Calculus [BibTeX] |
1976 | Theoretical Computer Science Vol. 2, pp. 323-337 |
article | URL |

BibTeX:
@article{Dez:76, author = {M. Dezani-Ciancaglini}, title = {Characterization of Normal Forms Possesing Inverse in the $beta eta$-Calculus}, journal = {Theoretical Computer Science}, year = {1976}, volume = {2}, pages = {323--337}, note = { http://dx.doi.org/10.1016/0304-3975(76)90085-2Electronic Edition}, url = {http://dx.doi.org/10.1016/0304-3975(76)90085-2} } |
|||||

Dougherty, D. | Some Lambda Calculi with Categorical Sums and Products [BibTeX] |
1993 | Proceedings of Rewriting Techniques and Applications'93, pp. 137-151 | inproceedings | |

BibTeX:
@inproceedings{Dou:93, author = {D. Dougherty}, title = {Some Lambda Calculi with Categorical Sums and Products}, booktitle = {Proceedings of Rewriting Techniques and Applications'93}, year = {1993}, pages = {137--151}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6064Electronic Edition} } |
|||||

Dougherty, D.J. | Some lambda calculi with categorical sums and products [BibTeX] |
1993 | Vol. 690Proceedings of the 5th International Conference on Rewriting Techniques and Applications (RTA-93), pp. 137-151 |
inproceedings | |

BibTeX:
@inproceedings{DD93, author = {Daniel J. Dougherty}, title = {Some lambda calculi with categorical sums and products}, booktitle = {Proceedings of the 5th International Conference on Rewriting Techniques and Applications (RTA-93)}, publisher = {Springer-Verlag}, year = {1993}, volume = {690}, pages = {137--151} } |
|||||

Ehrhard, T. & Regnier, L. | The differential lambda-calculus [BibTeX] |
2003 | Theoretical Computer Science Vol. 309(1-3), pp. 1-41 |
article | |

BibTeX:
@article{TELR03, author = {Thomas Ehrhard and Laurent Regnier}, title = {The differential lambda-calculus}, journal = {Theoretical Computer Science}, year = {2003}, volume = {309}, number = {1--3}, pages = {1--41} } |
|||||

Fettig, R. & Loechner, B. | Unification of Higher-Order Patterns in a Simply Typed Lambda-Calculus with Finite Products and Terminal Type [BibTeX] |
1996 | Lecture Notes in Computer Science Vol. 1103, pp. 347-?? |
article | |

BibTeX:
@article{RFBL:96, author = {R. Fettig and B. Loechner}, title = {Unification of Higher-Order Patterns in a Simply Typed Lambda-Calculus with Finite Products and Terminal Type}, journal = {Lecture Notes in Computer Science}, year = {1996}, volume = {1103}, pages = {347--??} } |
|||||

Fiore, M., Cosmo, R.D. & Balat, V. | Remarks on isomorphisms in typed lambda calculi with empty and sum types [BibTeX] |
2002 | Proceedings of Logic in Computer Science'02, pp. 147-156 | inproceedings | |

BibTeX:
@inproceedings{FCB:02, author = {M. Fiore and R. Di Cosmo and V. Balat}, title = {Remarks on isomorphisms in typed lambda calculi with empty and sum types}, booktitle = {Proceedings of Logic in Computer Science'02}, publisher = {IEEE Computer Society}, year = {2002}, pages = {147--156}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.13.9611Electronic Edition} } |
|||||

de Groote, P. & Salvati, S. | Higher-Order Matching in the Linear lambda-calculus with Pairing [BibTeX] |
2004 | Vol. 3210CSL, pp. 220-234 |
inproceedings | URL |

BibTeX:
@inproceedings{PGSS:04, author = {Philippe de Groote and Sylvain Salvati}, title = {Higher-Order Matching in the Linear lambda-calculus with Pairing}, booktitle = {CSL}, publisher = {Springer}, year = {2004}, volume = {3210}, pages = {220--234}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3210&spage=220} } |
|||||

Hindley, J.R. & Seldin, J.P. | Introduction or Combinators and Lambda Calculus [BibTeX] |
1986 | book | ||

BibTeX:
@book{HS:86, author = {J. R. Hindley and J. P. Seldin}, title = {Introduction or Combinators and Lambda Calculus}, publisher = {London Mathematical Society Student Texts 1, Cambridge University Press}, year = {1986} } |
|||||

Huet, G. | A Unification Algorithm for Typed $-Calculus [BibTeX] |
1975 | Theoretical Computer Science Vol. 1, pp. 27-57 |
article | URL |

BibTeX:
@article{Hue:75, author = {G. Huet}, title = {A Unification Algorithm for Typed $-Calculus}, journal = {Theoretical Computer Science}, year = {1975}, volume = {1}, pages = {27--57}, note = {http://dx.doi.org/10.1016/0304-3975(75)90011-0Electronic Edition}, url = {http://dx.doi.org/10.1016/0304-3975(75)90011-0} } |
|||||

Hustadt, U. | Unification and Matching in Church's Original Lambda Calculus [BibTeX] |
92 | (MPI-92-219) | techreport | URL |

BibTeX:
@techreport{UH:92, author = {Ullrich Hustadt}, title = {Unification and Matching in Church's Original Lambda Calculus}, year = {92}, number = {MPI-92-219}, url = {ftp://ftp.mpi-sb.mpg.de/pub/papers/reports/MPI-I-92-219.dvi.Z} } |
|||||

Jung, A. & Tiuryn, J. | A New Characterization of Lambda Definability [BibTeX] |
1993 | TLCA, pp. 245-257 | inproceedings | |

BibTeX:
@inproceedings{AJJT:93, author = {Achim Jung and Jerzy Tiuryn}, title = {A New Characterization of Lambda Definability}, booktitle = {TLCA}, year = {1993}, pages = {245-257} } |
|||||

Kamareddine, F. | Reviewing the Classical and the de Bruijn Notation for [lambda]-calculus and Pure Type Systems [BibTeX] |
2001 | Journal of Logic and Computation Vol. 11(3), pp. 363-394 |
article | URL |

BibTeX:
@article{FK:01, author = {Fairouz Kamareddine}, title = {Reviewing the Classical and the de Bruijn Notation for [lambda]-calculus and Pure Type Systems}, journal = {Journal of Logic and Computation}, year = {2001}, volume = {11}, number = {3}, pages = {363--394}, url = {http://www3.oup.co.uk/logcom/hdb/Volume_11/Issue_03/110363.sgm.abs.html} } |
|||||

Lincoln, P. & Mitchell, J. | Operational Aspects of Linear Lambda Calculus [BibTeX] |
1992 | Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, pp. 235-247 | inproceedings | |

BibTeX:
@inproceedings{PLJM:92, author = {P. Lincoln and J. Mitchell}, title = {Operational Aspects of Linear Lambda Calculus}, booktitle = {Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science}, publisher = {IEEE Computer Society Press}, year = {1992}, pages = {235--247} } |
|||||

Loader, R. | The Undecidability of lambda-Definability [BibTeX] |
1999 | misc | ||

BibTeX:
@misc{Lo:99, author = {R. Loader}, title = {The Undecidability of lambda-Definability}, year = {1999}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.6860Electronic Edition} } |
|||||

Miller, D. | Unification of Simply Typed Lambda-Terms as Logic Programming [BibTeX] |
1991 | Proc. Int. Conference on Logic Programming (Paris), pp. 255-269 | inproceedings | |

BibTeX:
@inproceedings{DM:91b, author = {D. Miller}, title = {Unification of Simply Typed Lambda-Terms as Logic Programming}, booktitle = {Proc. Int. Conference on Logic Programming (Paris)}, publisher = {MIT Press}, year = {1991}, pages = {255--269} } |
|||||

Miller, D. | A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification [BibTeX] |
1991 | Journal of Logic and Computation Vol. 1, pp. 253 - 281 |
article | |

BibTeX:
@article{Mil:91, author = {D. Miller}, title = {A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification}, journal = {Journal of Logic and Computation}, year = {1991}, volume = {1}, pages = {253 -- 281}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.8958Electronic Edition } } |
|||||

Padovani, V. | On equivalence classes of interpolation equations [BibTeX] |
1995 | Lecture Notes in Computer Science Vol. 902Second International Conference on Typed Lambda Calculi and Applications, TLCA '95 , pp. 335-?? |
inproceedings | DOI |

BibTeX:
@inproceedings{Pad:95, author = {V. Padovani}, title = {On equivalence classes of interpolation equations}, booktitle = {Second International Conference on Typed Lambda Calculi and Applications, TLCA '95 }, journal = {Lecture Notes in Computer Science}, publisher = {Springer Verlag}, year = {1995}, volume = {902}, pages = {335--??}, note = {http://dx.doi.org/10.1007/BFb0014063Electronic Edition}, doi = {http://dx.doi.org/10.1007/BFb0014063} } |
|||||

Pierce, B.C. | Foundational Calculi for Programming Languages | 1996 | misc | URL | |

Abstract: Introduction In the mid 1960s, Landin observed that a complex programming language can be understood in terms of a tiny "core language" capturing the essential mechanisms of some programming, style together with a collection of convenient "derived forms" whose behavior is understood by translating them into the core (cf. [ Tennent, 1981 ] ). Landin's core language was the lambdacalculus, a formal system in which all computation is reduced to the basic operations of function definition and application. Since the 60s, the lambda-calculus has seen widespread use in the specification of programming language features, language design and implementation, and the study of type systems. Its importance arises from the fact that it can be viewed simultaneously as a simple programming language in which computations can be described and as a mathematical object about which rigorous statements can be proved. The lambda-calculus has a strong claim to be a | |||||

BibTeX:
@misc{BP:96, author = {Benjamin C. Pierce}, title = {Foundational Calculi for Programming Languages}, year = {1996}, url = {http://citeseer.ist.psu.edu/55202.html; http://www.cs.indiana.edu/ftp/pierce/crchandbook.ps.gz} } |
|||||

S. Salvati, P. d.G. | On the complexity of higher-order matching in the linear lambda-calculus [BibTeX] |
2003 | RTAŽ03: Rewriting Techniques and Applications, 14th International Conference,, pp. 234-245 | inproceedings | URL |

BibTeX:
@inproceedings{SG:03, author = {S. Salvati, P. de Groote}, title = {On the complexity of higher-order matching in the linear lambda-calculus}, booktitle = {RTAŽ03: Rewriting Techniques and Applications, 14th International Conference,}, publisher = {Springer}, year = {2003}, pages = {234--245}, note = {http://link.springer.de/link/service/series/0558/bibs/2706/27060234.htmElectronic Edition}, url = {http://link.springer.de/link/service/series/0558/bibs/2706/27060234.htm} } |
|||||

Selinger, P. | Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus [BibTeX] |
2001 | Mathematical Structures in Computer Science Vol. 11(2), pp. 207-260 |
article | |

BibTeX:
@article{Sel:01, author = {Peter Selinger}, title = {Control Categories and Duality: On the Categorical Semantics of the Lambda-Mu Calculus}, journal = {Mathematical Structures in Computer Science}, year = {2001}, volume = {11}, number = {2}, pages = {207-260}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.389Electronic Edition} } |
|||||

Statman, R. | On the lambda Y calculus [BibTeX] |
2004 | Annals of.Pure and Applied Logic Vol. 130(1-3), pp. 325-337 |
article | URL |

BibTeX:
@article{RS:04, author = {Richard Statman}, title = {On the lambda Y calculus}, journal = {Annals of.Pure and Applied Logic}, year = {2004}, volume = {130}, number = {1-3}, pages = {325--337}, url = {http://dx.doi.org/10.1016/j.apal.2004.04.00} } |
|||||

Statman, R. | Completeness, Invariance and $-definability [BibTeX] |
1982 | Journal of Symbolic Logic Vol. 47, pp. 17-26 |
article | |

BibTeX:
@article{RS:82, author = {R. Statman}, title = {Completeness, Invariance and $-definability}, journal = {Journal of Symbolic Logic}, year = {1982}, volume = {47}, pages = {17--26} } |
|||||

Statman, R. | On the Existence of Closed Terms in the Typed $ Calculus II: Transformations of Unification Problems [BibTeX] |
1981 | Theoretical Computer Science Vol. 15(3), pp. 329-338 |
article | DOI |

BibTeX:
@article{Sta:81, author = {R. Statman}, title = {On the Existence of Closed Terms in the Typed $ Calculus II: Transformations of Unification Problems}, journal = {Theoretical Computer Science}, year = {1981}, volume = {15}, number = {3}, pages = {329--338}, note = {http://dx.doi.org/10.1016/0304-3975(81)90086-4Electronic Edition}, doi = {http://dx.doi.org/10.1016/0304-3975(81)90086-4} } |
|||||

Statman, R. | On the Existence of Closed Terms in the Typed $-Calculus I [BibTeX] |
1980 | To H.~B.~Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 511-534 | incollection | |

BibTeX:
@incollection{Sta:80, author = {R. Statman}, title = {On the Existence of Closed Terms in the Typed $-Calculus I}, booktitle = {To H.~B.~Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}, publisher = {Academic Press}, year = {1980}, pages = {511--534} } |
|||||

Stirling, C. | Model-Checking Games for Typed Lambda-Calculi [BibTeX] |
2007 | Electronic Notes in Theoretical Computer Science Vol. 172(172), pp. 589-609 |
article | DOI |

BibTeX:
@article{Col:07, author = {Stirling, C.}, title = {Model-Checking Games for Typed Lambda-Calculi}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2007}, volume = {172}, number = {172}, pages = {589-609}, note = {http://dx.doi.org/10.1016/j.entcs.2007.02.021Electronic Edition}, doi = {http://dx.doi.org/10.1016/j.entcs.2007.02.021} } |
|||||

Turing, A. | Computability and $-definability [BibTeX] |
1937 | Journal Symbolic Logic Vol. 2(4), pp. 153-163 |
article | URL |

BibTeX:
@article{Tur:37, author = {A. Turing}, title = {Computability and $-definability}, journal = {Journal Symbolic Logic}, year = {1937}, volume = {2}, number = {4}, pages = {153--163}, note = {http://www.jstor.org/stable/2268280Electronic Edition}, url = {http://www.jstor.org/stable/2268280} } |
|||||

Yoshinaka, R. | Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete [BibTeX] |
2005 | RTA: Rewriting Techniques and Applications, 1987, LNCS 256 | inproceedings | |

BibTeX:
@inproceedings{RY:05, author = {Roy Yoshinaka}, title = {Higher-Order Matching in the Linear Lambda Calculus in the Absence of Constants Is NP-Complete}, booktitle = {RTA: Rewriting Techniques and Applications, 1987, LNCS 256}, year = {2005} } |

Created by JabRef on 10/12/2008.