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

A. Alimarine, S. Smetsers, A. v.W.M. v.E. & Plasmeijer, R. | There and back again: arrows for invertible programming [BibTeX] |
2005 | Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, pp. 86-97 | inproceedings | DOI |

BibTeX:
@inproceedings{ASvvP:05, author = {A. Alimarine, S. Smetsers, A. van Weelden, M. van Eekelen and R. Plasmeijer}, title = {There and back again: arrows for invertible programming}, booktitle = {Haskell '05: Proceedings of the 2005 ACM SIGPLAN workshop on Haskell}, publisher = {ACM Press}, year = {2005}, pages = {86--97}, note = {http://doi.acm.org/10.1145/1088348.1088357Electronic Edition}, doi = {http://doi.acm.org/10.1145/1088348.1088357} } |
|||||

Abramsky, S. | A structural approach to reversible computation [BibTeX] |
2005 | Theoretical Computer Science Vol. 347(3), pp. 441-464 |
article | URL |

BibTeX:
@article{SA:05, author = {Samson Abramsky}, title = {A structural approach to reversible computation}, journal = {Theoretical Computer Science}, year = {2005}, volume = {347}, number = {3}, pages = {441--464}, url = {http://dx.doi.org/10.1016/j.tcs.2005.07.002} } |
|||||

Abramsky, S. | Semantics and Interaction [BibTeX] |
1996 | Semantics and Logics of Computation | inproceedings | |

BibTeX:
@inproceedings{Sam:96, author = {Samson Abramsky}, title = {Semantics and Interaction}, booktitle = {Semantics and Logics of Computation}, publisher = {Springer-Verlag}, year = {1996}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.49.9567Electronic Edition} } |
|||||

Abramsky, S. | Computational Interpretations of Linear Logic [BibTeX] |
1993 | Theoretical Computer Science Vol. 111(1-2), pp. 3-57 |
article | |

BibTeX:
@article{SA:93, author = {S. Abramsky}, title = {Computational Interpretations of Linear Logic}, journal = {Theoretical Computer Science}, year = {1993}, volume = {111}, number = {1-2}, pages = {3--57} } |
|||||

Ackermann, W. | Mengentheoretische Begründung der Logik [BibTeX] |
1937 | Mathematische Annalen Vol. 114, pp. 305-315 |
article | |

BibTeX:
@article{Ack:37, author = {W. Ackermann}, title = {Mengentheoretische Begründung der Logik}, journal = {Mathematische Annalen}, year = {1937}, volume = {114}, pages = {305--315} } |
|||||

Aho, A.V., Hopcroft, J.E. & Ullman, J.D. | The design and analysis of computer algorithms [BibTeX] |
1974 | book | ||

BibTeX:
@book{AHU:72, author = {A. V. Aho and J. E. Hopcroft and J. D. Ullman}, title = {The design and analysis of computer algorithms}, publisher = {Addison-Wesley}, year = {1974} } |
|||||

Alimarine, A., Smetsers, S., van Weelden, A., van Eekelen, M.C.J.D. & Plasmeijer, R. | There and back again: arrows for invertible programming [BibTeX] |
2005 | Haskell, pp. 86-97 | inproceedings | URL |

BibTeX:
@inproceedings{AASSAvW:05, author = {Artem Alimarine and Sjaak Smetsers and Arjen van Weelden and Marko C. J. D. van Eekelen and Rinus Plasmeijer}, title = {There and back again: arrows for invertible programming}, booktitle = {Haskell}, publisher = {ACM}, year = {2005}, pages = {86--97}, url = {http://doi.acm.org/10.1145/1088348.1088357} } |
|||||

Allender, E., Catalunya, U.P.D. & Immerman, N. | A First-Order Isomorphism Theorem | 1993 | misc | URL | |

Abstract: We show that for most complexity classes of interest, all sets complete under firstorder projections (fops) are isomorphic under first-order isomorphisms. That is, a very restricted version of the Berman-Hartmanis Conjecture holds. Since "natural" complete problems seem to stay complete via fops, this indicates that up to first-order isomorphism there is only one "natural" complete problem for each "nice" complexity class. 1 Introduction In 1977 Berman and Hartmanis noticed that all NP complete sets that they knew of were polynomial-time isomorphic, [BH77]. They made their now-famous isomorphism conjecture: namely that all NP complete sets are polynomial-time isomorphic. This conjecture has engendered a large amount of work (cf. [KMR90, You] for surveys). The isomorphism conjecture was made using the notion of NP completeness via polynomialtime, many-one reductions because that was the standard definition at the time. In [Coo], A preliminary version of this work appeared in Proc. 1... |
|||||

BibTeX:
@misc{EANI:93, author = {Eric Allender and U. Polit`ecnica De Catalunya and Neil Immerman}, title = {A First-Order Isomorphism Theorem}, year = {1993}, url = {http://citeseer.ist.psu.edu/47536.html; http://www.cs.umass.edu/~immerman/pub/isomorphism.ps} } |
|||||

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} } |
|||||

Andreev, A.E. & Soloviev, S. | A Deciding Algorithm for Linear Isomorphism of Types with Complexity O (n log$^2$(n)) [BibTeX] |
1997 | Vol. 1290CTCS, pp. 197-209 |
inproceedings | |

BibTeX:
@inproceedings{AASS:97, author = {Alexander E. Andreev and Sergei Soloviev}, title = {A Deciding Algorithm for Linear Isomorphism of Types with Complexity O (n log$^2$(n))}, booktitle = {CTCS}, publisher = {Springer}, year = {1997}, volume = {1290}, pages = {197--209} } |
|||||

Ariola, Z.M. & Arvind | A Syntactic Approach to Program Transformations [BibTeX] |
1991 | PEPM, pp. 116-129 | inproceedings | |

BibTeX:
@inproceedings{ZAA:91, author = {Zena M. Ariola and Arvind}, title = {A Syntactic Approach to Program Transformations}, booktitle = {PEPM}, year = {1991}, pages = {116--129} } |
|||||

Atanassow, F. & Jeuring, J. | Inferring Type Isomorphisms Generically [BibTeX] |
2004 | Vol. 3125MPC, pp. 32-53 |
inproceedings | URL |

BibTeX:
@inproceedings{FAJJ:04, author = {Frank Atanassow and Johan Jeuring}, title = {Inferring Type Isomorphisms Generically}, booktitle = {MPC}, publisher = {Springer}, year = {2004}, volume = {3125}, pages = {32--53}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3125&spage=32} } |
|||||

AUTOMATH | The AUTOMATH project [BibTeX] |
1967 | other | URL | |

BibTeX:
@other{Automath, author = {AUTOMATH}, title = {The AUTOMATH project}, year = {1967}, note = {http://www.win.tue.nl/automath/Website}, url = {http://www.win.tue.nl/automath/} } |
|||||

Baker, H.G. | A "Linear Logic" Quicksort [BibTeX] |
1994 | SIGPLAN Notices Vol. 29(2), pp. 13-18 |
article | |

BibTeX:
@article{HB:94, author = {Henry G. Baker}, title = {A "Linear Logic" Quicksort}, journal = {SIGPLAN Notices}, year = {1994}, volume = {29}, number = {2}, pages = {13--18} } |
|||||

Balat, V. & Cosmo, R.D. | A Linear Logical View of Linear Type Isomorphisms [BibTeX] |
1999 | Vol. 1683CSL, pp. 250-265 |
inproceedings | |

BibTeX:
@inproceedings{VBRdC:99, author = {Vincent Balat and Roberto Di Cosmo}, title = {A Linear Logical View of Linear Type Isomorphisms}, booktitle = {CSL}, publisher = {Springer}, year = {1999}, volume = {1683}, pages = {250--265} } |
|||||

Balat, V. & Danvy, O. | Memoization in Type-Directed Partial Evaluation [BibTeX] |
2002 | Lecture Notes in Computer Science Vol. 2487, pp. 78-?? |
article | URL |

BibTeX:
@article{VBOD:02, author = {Vincent Balat and Olivier Danvy}, title = {Memoization in Type-Directed Partial Evaluation}, journal = {Lecture Notes in Computer Science}, year = {2002}, volume = {2487}, pages = {78--??}, url = {http://link.springer.de/link/service/series/0558/bibs/2487/24870078.htm; http://link.springer.de/link/service/series/0558/papers/2487/24870078.pdf} } |
|||||

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} } |
|||||

Barthe, G. | A computational view of implicit coercions in Type theory [BibTeX] |
2005 | Mathematical Structures in Computer Science Vol. 15, pp. 839-874 |
article | DOI |

BibTeX:
@article{Bart:05, author = {Barthe, G.}, title = {A computational view of implicit coercions in Type theory}, journal = {Mathematical Structures in Computer Science}, year = {2005}, volume = {15}, pages = {839-874}, note = {http://dx.doi.org/10.1017/S0960129505004901Electronic Edition}, doi = {http://dx.doi.org/10.1017/S0960129505004901} } |
|||||

Barthe, G. | Implicit Coercions in Type Systems [BibTeX] |
1996 | Vol. 1512International Workshop TYPES'96, pp. 1-15 |
inproceedings | |

BibTeX:
@inproceedings{Bart:96, author = {G. Barthe}, title = {Implicit Coercions in Type Systems}, booktitle = {International Workshop TYPES'96}, publisher = {Springer Verlag}, year = {1996}, volume = {1512}, pages = {1-15}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.9520Electronic Edition} } |
|||||

Barthe, G. & Pons, O. | Type Isomorphisms and Proof Reuse in Dependent Type Theory [BibTeX] |
2001 | Vol. 2030FoSSaCS, pp. 57-71 |
inproceedings | URL |

BibTeX:
@inproceedings{GBOP:01, author = {Gilles Barthe and Olivier Pons}, title = {Type Isomorphisms and Proof Reuse in Dependent Type Theory}, booktitle = {FoSSaCS}, publisher = {Springer}, year = {2001}, volume = {2030}, pages = {57--71}, url = {http://link.springer.de/link/service/series/0558/bibs/2030/20300057.htm} } |
|||||

Basin, D. | A term equality problem equivalent to Graph Isomorphism [BibTeX] |
1994 | Information Processing Letters Vol. 51(2), pp. 61-66 |
article | |

BibTeX:
@article{Bas:94, author = {D. Basin}, title = {A term equality problem equivalent to Graph Isomorphism}, journal = {Information Processing Letters}, year = {1994}, volume = {51}, number = {2}, pages = {61--66}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.7354Electronic Edition} } |
|||||

Bednarek, A.R. | A note on tree isomorphisms [BibTeX] |
1974 | Journal of Combinatorial Theory Series B Vol. 16, pp. 194-196 |
article | |

BibTeX:
@article{Bed:74, author = {A. R. Bednarek}, title = {A note on tree isomorphisms}, journal = {Journal of Combinatorial Theory Series B}, publisher = {Academic Press}, year = {1974}, volume = {16}, pages = {194--196}, note = {http://dx.doi.org/10.1016/0095-8956(74)90064-1Electronic Edition} } |
|||||

Bennett, C.H. | Logical Reversibility of Computation [BibTeX] |
1973 | IBM Journal of Research and Development Vol. 17(6), pp. 525-532 |
article | URL |

BibTeX:
@article{Ben:73, author = {C. H. Bennett}, title = {Logical Reversibility of Computation}, journal = {IBM Journal of Research and Development}, year = {1973}, volume = {17}, number = {6}, pages = {525--532}, note = {http://www.research.ibm.com/journal/rd/176/ibmrd1706G.pdfElectronic Edition}, url = {http://www.research.ibm.com/journal/rd/176/ibmrd1706G.pdf} } |
|||||

Berghofer, S. | Program Extraction in Simply-Typed Higher Order Logic [BibTeX] |
2002 | Vol. 2646TYPES, pp. 21-38 |
inproceedings | URL |

BibTeX:
@inproceedings{SB:02, author = {Stefan Berghofer}, title = {Program Extraction in Simply-Typed Higher Order Logic}, booktitle = {TYPES}, publisher = {Springer}, year = {2002}, volume = {2646}, pages = {21--38}, url = {http://link.springer.de/link/service/series/0558/bibs/2646/26460021.htm} } |
|||||

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} } |
|||||

Lang, B. | Matching with Multiplication (Extended Abstract) [BibTeX] |
2005 | Mathematical Structures in Computer Science Vol. 15, pp. 959-968 |
article | DOI |

BibTeX:
@article{BL:05, author = {Bernard Lang,}, title = {Matching with Multiplication (Extended Abstract)}, journal = {Mathematical Structures in Computer Science}, year = {2005}, volume = {15}, pages = {959-968}, note = {http://dx.doi.org/10.1017/S0960129505004883Electronic Edition}, doi = {http://dx.doi.org/10.1017/S0960129505004883} } |
|||||

Betarte, G. | Dependent Record Types and Algebraic Structures in Type Theory [BibTeX] |
1998 | School: Department of Computing Science, Chalmers University of Technology and University of Göteborg |
phdthesis | |

BibTeX:
@phdthesis{Bet:98, author = {G. Betarte}, title = {Dependent Record Types and Algebraic Structures in Type Theory}, school = {Department of Computing Science, Chalmers University of Technology and University of Göteborg}, year = {1998} } |
|||||

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} } |
|||||

Bird, R., Gibbons, J. & Jones, G. | Program Optimisation, Naturally [BibTeX] |
2000 | Millenial Perspectives in Computer Science. Palgrave | inproceedings | DOI |

BibTeX:
@inproceedings{BGJ:00, author = {R. Bird and J. Gibbons and G. Jones}, title = {Program Optimisation, Naturally}, booktitle = {Millenial Perspectives in Computer Science. Palgrave}, year = {2000}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2331Electronic Edition}, doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2331} } |
|||||

Bird, R.S. & Moor, O.D. | Algebra of Programming [BibTeX] |
1997 | Vol. 100 |
book | URL |

BibTeX:
@book{BO:97, author = {R. S. Bird and O. De Moor}, title = {Algebra of Programming}, publisher = {Prentice-Hall International Series in Computer Science}, year = {1997}, volume = {100}, note = { http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/Project's Webpage}, url = {http://www.comlab.ox.ac.uk/oucl/publications/books/algebra/} } |
|||||

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} } |
|||||

Bruce & Longo | Provable Isomorphisms and Domain Equations in Models of Typed Languages [BibTeX] |
1985 | STOC: ACM Symposium on Theory of Computing (STOC) | inproceedings | |

BibTeX:
@inproceedings{KBGL:85, author = {Bruce and Longo}, title = {Provable Isomorphisms and Domain Equations in Models of Typed Languages}, booktitle = {STOC: ACM Symposium on Theory of Computing (STOC)}, year = {1985} } |
|||||

Bruce, K.B., di Cosmo, R. & Longo, G. | Provable Isomorphisms of Types [BibTeX] |
1990 | (90-14) | techreport | |

BibTeX:
@techreport{KBRdCGL:90, author = {Kim B. Bruce and Roberto di Cosmo and Giuseppe Longo}, title = {Provable Isomorphisms of Types}, year = {1990}, number = {90-14} } |
|||||

Bruce, K.B., Cosmo, R.D. & Longo, G. | Provable isomorphisms of types [BibTeX] |
1991 | Mathematical Structures in Computer Science Vol. 2(2), pp. 231-247 |
article | URL |

BibTeX:
@article{BDL:91, author = {K. B. Bruce and R. Di Cosmo and G. Longo}, title = {Provable isomorphisms of types}, journal = {Mathematical Structures in Computer Science}, year = {1991}, volume = {2}, number = {2}, pages = {231--247}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353Electronic Edition}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353} } |
|||||

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} } |
|||||

Burstall, R.M. & Darlington, J. | A transformational system for developing recursive programs [BibTeX] |
1977 | Journal of the Associattion of Computing Machinery Vol. 24(1), pp. 44-67 |
article | URL |

BibTeX:
@article{BD:77, author = {R. M. Burstall and J. Darlington}, title = {A transformational system for developing recursive programs}, journal = {Journal of the Associattion of Computing Machinery}, year = {1977}, volume = {24}, number = {1}, pages = {44--67}, note = {http://doi.acm.org/10.1145/321992.321996Electronic Edition}, url = {http://portal.acm.org/citation.cfm?id=321996} } |
|||||

Böhm, C. & Dezani-Ciancaglini, M. | Combinatorial Problems, Combinator Equations and Normal Forms [BibTeX] |
1974 | Automata, Languages and Programming, Second Colloquium, Saarbrücken Vol. 14Proceedings of the 2nd Colloquium on Automata, Languages and Programming, pp. 185-199 |
inproceedings | |

BibTeX:
@inproceedings{BD:74, author = {C. Böhm and M. Dezani-Ciancaglini}, title = {Combinatorial Problems, Combinator Equations and Normal Forms}, booktitle = {Proceedings of the 2nd Colloquium on Automata, Languages and Programming}, journal = {Automata, Languages and Programming, Second Colloquium, Saarbrücken}, publisher = {Lecture Notes in Computer Science, Springer-Verlag}, year = {1974}, volume = {14}, pages = {185--199}, note = {http://portal.acm.org/citation.cfm?id=646230.681874Electronic Edition} } |
|||||

Cai, J. & Paige, R. | Multiset Discrimination - A Method for Implementing Programming Language Systems without Hashing [BibTeX] |
1992 | (TR1992-609) | techreport | |

BibTeX:
@techreport{CP:02, author = {J. Cai and R. Paige}, title = {Multiset Discrimination - A Method for Implementing Programming Language Systems without Hashing}, year = {1992}, number = {TR1992-609}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.5597Electronic Edition} } |
|||||

Cardelli, L. | Type systems [BibTeX] |
1996 | ACM Computing Surveys Vol. 28(1), pp. 263-264 |
article | URL |

BibTeX:
@article{Car:96, author = {L. Cardelli}, title = {Type systems}, journal = {ACM Computing Surveys}, year = {1996}, volume = {28}, number = {1}, pages = {263--264}, note = {http://doi.acm.org/10.1145/234313.234418Electronic Edition}, url = {http://www.acm.org/pubs/citations/journals/surveys/1996-28-1/p263-cardelli/} } |
|||||

Cervesato, I. & Pfenning, F. | Linear Higher-Order Pre-Unification [BibTeX] |
1997 | Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS'97), pp. 422-433 | inproceedings | |

BibTeX:
@inproceedings{Cel:97, author = {Iliano Cervesato and Frank Pfenning}, title = {Linear Higher-Order Pre-Unification}, booktitle = {Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS'97)}, publisher = {IEEE Computer Society Press}, year = {1997}, pages = {422--433}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.4249Electronic Edition} } |
|||||

Chaudhary, S. & Gordon, G. | Tutte polynomials for trees [BibTeX] |
1991 | Journal Graph Theory Vol. 15(3), pp. 317-331 |
article | |

BibTeX:
@article{SCGG:91, author = {Sharad Chaudhary and Gary Gordon}, title = {Tutte polynomials for trees}, journal = {Journal Graph Theory}, publisher = {John Wiley & Sons}, year = {1991}, volume = {15}, number = {3}, pages = {317--331} } |
|||||

Chemouil, Davis, M. | Isomorphisms of simple inductive types through extensional rewriting [BibTeX] |
2005 | Mathematical Structures in Computer Science Vol. 15, pp. 875-915 |
article | DOI |

BibTeX:
@article{Che:05, author = {Chemouil, Davis, M.}, title = {Isomorphisms of simple inductive types through extensional rewriting}, journal = {Mathematical Structures in Computer Science}, year = {2005}, volume = {15}, pages = {875-915}, note = {http://dx.doi.org/10.1017/S0960129505004950Electronic Edition}, doi = {http://dx.doi.org/10.1017/S0960129505004950} } |
|||||

Chi, Y., Yang, Y. & Muntz, R.R. | Canonical forms for labelled trees and their applications in frequent subtree mining [BibTeX] |
2005 | Knowledge and Information Systems. Vol. 8(2), pp. 203-234 |
article | DOI |

BibTeX:
@article{CYM:05, author = {Yun Chi and Yirong Yang and Richard R. Muntz}, title = {Canonical forms for labelled trees and their applications in frequent subtree mining}, journal = {Knowledge and Information Systems.}, year = {2005}, volume = {8}, number = {2}, pages = {203-234}, doi = {http://dx.doi.org/10.1007/s10115-004-0180-7} } |
|||||

Chiba, Y. & Aoto, T. | RAPT: A Program Transformation System Based on Term Rewriting (system description) [BibTeX] |
2006 | Term Rewriting and Applications, 17th International Conference, RTA-06, pp. 267-276 | inproceedings | |

BibTeX:
@inproceedings{YCTA:06, author = {Y. Chiba and T. Aoto}, title = {RAPT: A Program Transformation System Based on Term Rewriting (system description)}, booktitle = {Term Rewriting and Applications, 17th International Conference, RTA-06}, publisher = {Springer}, year = {2006}, pages = {267--276} } |
|||||

Chitil, O. | Type Inference Builds a Short Cut to Deforestation [BibTeX] |
1999 | ICFP, pp. 249-260 | inproceedings | URL |

BibTeX:
@inproceedings{OC:99, author = {Olaf Chitil}, title = {Type Inference Builds a Short Cut to Deforestation}, booktitle = {ICFP}, year = {1999}, pages = {249-260}, url = {http://doi.acm.org/10.1145/317636.317907} } |
|||||

Church, A. | A formulation of a simple theory of types [BibTeX] |
1940 | Journal of Symbolic Logic Vol. 5, pp. 56-68 |
article | URL |

BibTeX:
@article{Ch:40, author = {A. Church}, title = {A formulation of a simple theory of types}, journal = {Journal of Symbolic Logic}, year = {1940}, volume = {5}, pages = {56--68}, note = {http://www.jstor.org/stable/2266866Electronic Edition}, url = {http://www.jstor.org/stable/2266866} } |
|||||

Church, A. | A Set of Postulates for the Foundation of Logic Part II [BibTeX] |
1933 | Annals of Mathematics Vol. 34(2), pp. 839-864 |
article | |

BibTeX:
@article{Ch:33, author = {A. Church}, title = {A Set of Postulates for the Foundation of Logic Part II}, journal = {Annals of Mathematics}, year = {1933}, volume = {34}, number = {2}, pages = {839--864} } |
|||||

Church, A. | A Set of Postulates for the Foundation of Logic Part I [BibTeX] |
1932 | Annals of Mathematics Vol. 33(2), pp. 346-366 |
article | URL |

BibTeX:
@article{Ch:32, author = {A. Church}, title = {A Set of Postulates for the Foundation of Logic Part I}, journal = {Annals of Mathematics}, year = {1932}, volume = {33}, number = {2}, pages = {346--366}, note = {http://www.jstor.org/stable/1968702Electronic Edition}, url = {http://www.jstor.org/stable/1968702} } |
|||||

Church, A. & Rosser, J.B. | Some properties of conversion [BibTeX] |
1936 | Transactions of the American Mathematical Society Vol. 39, pp. 472-482 |
article | URL |

BibTeX:
@article{CR:36, author = {A. Church and J. B. Rosser}, title = {Some properties of conversion}, journal = {Transactions of the American Mathematical Society}, year = {1936}, volume = {39}, pages = {472--482}, note = {http://www.jstor.org/stable/2268573Electronic Edition}, url = {http://www.jstor.org/stable/2268573} } |
|||||

Comon, H. & Jurski, Y. | Higher-Order Matching and Tree Automata [BibTeX] |
1997 | CSL, pp. 157-176 | inproceedings | |

BibTeX:
@inproceedings{HCYJ:97, author = {Hubert Comon and Yan Jurski}, title = {Higher-Order Matching and Tree Automata}, booktitle = {CSL}, year = {1997}, pages = {157-176} } |
|||||

Considine, J. | Efficient Hash-Consing of Recursive Types | 2000 | (2000-006) | techreport | URL |

Abstract: Efficient storage of types within a compiler is necessary to avoid large blowups in space during compilation. Recursive types in particular are important to consider, as naive representations of recursive types may be arbitrarily larger than necessary through unfolding. Hash-consing has been used to efficiently store non-recursive types. Deterministic finite automata techniques have been used to efficiently perform various operations on recursive types. We present a new system for storing recursive types combining hash-consing and deterministic finite automata techniques. The space requirements are linear in the number of distinct types. Both update and lookup operations take polynomial time and linear space and type equality can be checked in constant time once both types are in the system. |
|||||

BibTeX:
@techreport{JC:00, author = {Jeffrey Considine}, title = {Efficient Hash-Consing of Recursive Types}, year = {2000}, number = {2000-006}, url = {http://www.cs.bu.edu/techreports/2000-006-hashconsing-recursive-types.ps.Z} } |
|||||

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} } |
|||||

Constable, R. | The Metaprl proof assistant [BibTeX] |
1981 | other | ||

BibTeX:
@other{METAPRL, author = {Robert Constable}, title = {The Metaprl proof assistant}, year = {1981}, note = { http://metaprl.org/Website} } |
|||||

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} } |
|||||

Cosmo, R.D., Pottier, F. & Rémy, D. | Subtyping Recursive Types Modulo Associative Commutative Products [BibTeX] |
2005 | Vol. 3461TLCA, pp. 179-193 |
inproceedings | URL |

BibTeX:
@inproceedings{DiCFPDR05, author = {Roberto Di Cosmo and Francois Pottier and Didier Rémy}, title = {Subtyping Recursive Types Modulo Associative Commutative Products}, booktitle = {TLCA}, publisher = {Springer}, year = {2005}, volume = {3461}, pages = {179--193}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3461&spage=179} } |
|||||

Cruz-Filipe, L. & Spitters, B. | Program Extraction from Large Proof Developments [BibTeX] |
2003 | Vol. 2758TPHOLs, pp. 205-220 |
inproceedings | URL |

BibTeX:
@inproceedings{LCBS:03, author = {Luís Cruz-Filipe and Bas Spitters}, title = {Program Extraction from Large Proof Developments}, booktitle = {TPHOLs}, publisher = {Springer}, year = {2003}, volume = {2758}, pages = {205--220}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=205} } |
|||||

Curien, P.L. | Notes on Game Semantics [BibTeX] |
2006 | unpublished | ||

BibTeX:
@unpublished{Cur:06, author = {Curien, Pierre Louis}, title = {Notes on Game Semantics}, year = {2006}, note = {http://www.pps.jussieu.fr/~curien/Game-semantics.pdfElectronic Edition} } |
|||||

Curry, H. | Functionality in combinatorial logic [BibTeX] |
1934 | Vol. 20Proceedings of National Academy of Sciences, pp. 584-590 |
inproceedings | |

BibTeX:
@inproceedings{Cu:34, author = {H. Curry}, title = {Functionality in combinatorial logic}, booktitle = {Proceedings of National Academy of Sciences}, year = {1934}, volume = {20}, pages = {584--590} } |
|||||

Curry, H.B. & Feys, R. | Combinatory Logic, Volume I [BibTeX] |
1958 | , pp. xvi+417 | book | |

BibTeX:
@book{CF:58, author = {H. B. Curry and R. Feys}, title = {Combinatory Logic, Volume I}, publisher = {North-Holland}, year = {1958}, pages = {xvi+417}, note = {Second printing 1968} } |
|||||

Curry, H.B., Hindley, J.R. & Seldin, J.P. | Combinatory Logic, Volume II [BibTeX] |
1972 | , pp. xiv+520 | book | |

BibTeX:
@book{CHS:72, author = {H. B. Curry and J. R. Hindley and J. P. Seldin}, title = {Combinatory Logic, Volume II}, publisher = {North-Holland}, year = {1972}, pages = {xiv+520} } |
|||||

Danos, V., Joinet, J. & Schellinx, H. | Computational isomorphisms in classical logic [BibTeX] |
2003 | Theoretical Computer Science Vol. 294(3), pp. 353 - 378 |
article | DOI |

BibTeX:
@article{DJS:98, author = {V. Danos and J.-B. Joinet and H. Schellinx}, title = {Computational isomorphisms in classical logic}, journal = {Theoretical Computer Science}, year = {2003}, volume = {294}, number = {3}, pages = {353 - 378}, note = {http://dx.doi.org/10.1016/S0304-3975(01)00148-7Electronic Edition}, doi = {http://dx.doi.org/10.1016/S0304-3975(01)00148-7} } |
|||||

Danos, V., Joinet, J. & Schellinx, H. | A new deconstructive logic: linear logic [BibTeX] |
1997 | Journal of Symbolic Logic Vol. 62(3), pp. 755-807 |
article | |

BibTeX:
@article{VDJJHS97, author = {V. Danos and J.-B. Joinet and H. Schellinx}, title = {A new deconstructive logic: linear logic}, journal = {Journal of Symbolic Logic}, year = {1997}, volume = {62}, number = {3}, pages = {755--807}, note = {footnotesize (Slightly revised version of the 1995 technical report with the same title)} } |
|||||

Danos, V., Joinet, J., Schellinx, H., Mathematique, E.D.L., Vii, U.P. & Instituut, M. | Computational Isomorphisms [BibTeX] |
2001 | misc | URL | |

BibTeX:
@misc{VDJJHS01, author = {Vincent Danos and Jean-baptiste Joinet and Harold Schellinx and Equipe De Logique Mathematique and Universite Paris Vii and Mathematisch Instituut}, title = {Computational Isomorphisms}, year = {2001}, url = {http://citeseer.ist.psu.edu/623841.html; http://www.logique.jussieu.fr/www.danos/psgz/cicl.ps.gz} } |
|||||

Davis, M. | Computability and Unsolvability [BibTeX] |
1982 | book | ||

BibTeX:
@book{Dav:82, author = {M. Davis}, title = {Computability and Unsolvability}, publisher = {Dover}, year = {1982}, note = {Previous edition 1958} } |
|||||

Davis, M. | Hilbert's Tenth Problem is unsolvable [BibTeX] |
1973 | The American Mathematical Monthly Vol. 80(3), pp. 233-269 |
article | URL |

BibTeX:
@article{Dav:73, author = {M. Davis}, title = {Hilbert's Tenth Problem is unsolvable}, journal = {The American Mathematical Monthly}, year = {1973}, volume = {80}, number = {3}, pages = {233--269}, note = {http://www.jstor.org/stable/2318447Electronic Edition}, url = {http://www.jstor.org/stable/2318447} } |
|||||

Delahaye, D. | Information Retrieval in a Coq Proof Library Using Type Isomorphisms [BibTeX] |
2000 | Lecture Notes in Computer Science Vol. 1956TYPES '99: Selected papers from the International Workshop on Types for Proofs and Programs, pp. 131-147 |
inproceedings | URL |

BibTeX:
@inproceedings{Del:00, author = {D. Delahaye}, title = {Information Retrieval in a Coq Proof Library Using Type Isomorphisms}, booktitle = {TYPES '99: Selected papers from the International Workshop on Types for Proofs and Programs}, journal = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, year = {2000}, volume = {1956}, pages = {131--147}, note = {http://link.springer.de/link/service/series/0558/bibs/1956/19560131.htmElectronic Edition}, url = {http://link.springer.de/link/service/series/0558/bibs/1956/19560131.htm} } |
|||||

Dershowitz, N., Jouannaud, J. & Klop, J.W. | Problems in Rewriting III [BibTeX] |
1995 | Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany), pp. 457-471 | inproceedings | |

BibTeX:
@inproceedings{NDJJJK:95, author = {Nachum Dershowitz and Jean-Pierre Jouannaud and Jan Willem Klop}, title = {Problems in Rewriting III}, booktitle = {Proceedings of the Sixth International Conference on Rewriting Techniques and Applications (Kaiserslautern, Germany)}, publisher = {Springer-Verlag}, year = {1995}, pages = {457--471} } |
|||||

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} } |
|||||

Dezani-Ciancaglini, M., Cosmo, R.D., Giovannetti, E. & Tatsuta, M. | On Isomorphisms of Intersection Types [BibTeX] |
2008 | Vol. 5213CSL, pp. 461-477 |
inproceedings | URL |

BibTeX:
@inproceedings{MDCRdCEGMT:08, author = {Mariangiola Dezani-Ciancaglini and Roberto Di Cosmo and Elio Giovannetti and Makoto Tatsuta}, title = {On Isomorphisms of Intersection Types}, booktitle = {CSL}, publisher = {Springer}, year = {2008}, volume = {5213}, pages = {461--477}, url = {http://dx.doi.org/10.1007/978-3-540-87531-4_33} } |
|||||

Doner, J. & Tarski, A. | An Extended Arithmetic of Ordinal Numbers [BibTeX] |
1969 | Fundamenta Mathematicae Vol. 65, pp. 95-127 |
article | |

BibTeX:
@article{DT:69, author = {J. Doner and A. Tarski}, title = {An Extended Arithmetic of Ordinal Numbers}, journal = {Fundamenta Mathematicae}, year = {1969}, volume = {65}, pages = {95--127} } |
|||||

Dosen, K. & Petric, Z. | The Typed Bohm Theorem [BibTeX] |
2001 | Electronic Notes in Theoretical Computer Science Vol. 50(2), pp. 119 - 131 |
article | URL |

BibTeX:
@article{KDZP:01, author = {Kosta Dosen and Zoran Petric}, title = {The Typed Bohm Theorem}, journal = {Electronic Notes in Theoretical Computer Science}, year = {2001}, volume = {50}, number = {2}, pages = {119 -- 131}, url = {http://www.elsevier.com/gej-ng/31/29/23/85/28/show/Products/notes/index.htt#003} } |
|||||

Dougherty & Subrahmanyam | Equality between Functionals in the Presence of Coproducts [BibTeX] |
2000 | Information and Computation Vol. 157, pp. 52 - 83 |
article | |

BibTeX:
@article{DDRS00, author = {Dougherty and Subrahmanyam}, title = {Equality between Functionals in the Presence of Coproducts}, journal = {Information and Computation}, year = {2000}, volume = {157}, pages = {52 -- 83} } |
|||||

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. & Martínez, C. | Unification and Matching Modulo Type Isomorphism [BibTeX] |
2004 | Proceedings of II International Workshop of Higher Order Rewriting | inproceedings | DOI |

BibTeX:
@inproceedings{DM:04, author = {D. Dougherty and C. Martínez}, title = {Unification and Matching Modulo Type Isomorphism}, booktitle = {Proceedings of II International Workshop of Higher Order Rewriting}, year = {2004}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353Electronic Edition}, doi = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.104.8353} } |
|||||

Dougherty, D. & Wierzbicki, T. | A Decidable Variant of Higher Order Matching [BibTeX] |
2002 | Vol. 256RTA '02: Proceedings of the 13th International Conference on Rewriting Techniques and Applications, pp. 340-351 |
inproceedings | |

BibTeX:
@inproceedings{DW:02, author = {D. Dougherty and T. Wierzbicki}, title = {A Decidable Variant of Higher Order Matching}, booktitle = {RTA '02: Proceedings of the 13th International Conference on Rewriting Techniques and Applications}, publisher = {Springer Verlag}, year = {2002}, volume = {256}, pages = {340--351}, note = {http://www.springerlink.com/link.asp?id=y0t2jwqnfucwju35Electronic 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} } |
|||||

Dowek, G. | Higher-Order Unification and Matching [BibTeX] |
2001 | Handbook of automated reasoning Vol. IIHandbook of Automated Reasoning, pp. 1009-1062 |
article | URL |

BibTeX:
@article{Dow:01, author = {G. Dowek}, title = {Higher-Order Unification and Matching}, booktitle = {Handbook of Automated Reasoning}, journal = {Handbook of automated reasoning}, publisher = {Elsevier Science}, year = {2001}, volume = {II}, pages = {1009--1062}, note = {http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=778525Electronic Edition}, url = {http://www.lix.polytechnique.fr/~dowek/Publi/unification.ps} } |
|||||

Dowek, G. | Third order matching is decidable [BibTeX] |
1994 | Annals of Pure and Applied Logic Vol. 69(2-3), pp. 135-155 |
article | URL |

BibTeX:
@article{Dow:94, author = {G. Dowek}, title = {Third order matching is decidable}, journal = {Annals of Pure and Applied Logic}, year = {1994}, volume = {69}, number = {2--3}, pages = {135--155}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6700Electronic Edition}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.6700} } |
|||||

Dowek, G. | The undecidability of pattern matching in calculi where primitive recursive functions are representable [BibTeX] |
1993 | Theoretical Computer Science Vol. 107, pp. 349-356 |
article | URL |

BibTeX:
@article{Dow:93, author = {G. Dowek}, title = {The undecidability of pattern matching in calculi where primitive recursive functions are representable}, journal = {Theoretical Computer Science}, publisher = {Elsevier Science Publishers B.V. (North Holland)}, year = {1993}, volume = {107}, pages = {349--356}, note = {http://dx.doi.org/10.1016/0304-3975(93)90175-SElectronic Edition}, url = {http://dx.doi.org/10.1016/0304-3975(93)90175-S} } |
|||||

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} } |
|||||

Elliott, C. | Higher-order Unification with Dependent Function Types [BibTeX] |
1989 | RTA, pp. 121-136 | inproceedings | |

BibTeX:
@inproceedings{CE:89, author = {Conal Elliott}, title = {Higher-order Unification with Dependent Function Types}, booktitle = {RTA}, year = {1989}, pages = {121-136} } |
|||||

Elliott, C.M. | Extensions and Applications of Higher-Order Unification [BibTeX] |
1990 | School: School of Computer Science, Carnegie Mellon University |
phdthesis | |

BibTeX:
@phdthesis{Eli:90, author = {C. M. Elliott}, title = {Extensions and Applications of Higher-Order Unification}, school = {School of Computer Science, Carnegie Mellon University}, year = {1990}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.73.5040Electronic Edition} } |
|||||

Farmer, W. | Simple second-order languages for which unification is undecidable [BibTeX] |
1991 | Theoretical Computer Science Vol. 87(1), pp. 25-41 |
article | DOI |

BibTeX:
@article{Far:91, author = {W. Farmer}, title = {Simple second-order languages for which unification is undecidable}, journal = {Theoretical Computer Science}, year = {1991}, volume = {87}, number = {1}, pages = {25--41}, note = {http://dx.doi.org/10.1016/0304-3975(91)90024-VElectronic Edition}, doi = {http://dx.doi.org/10.1016/0304-3975(91)90024-V} } |
|||||

Farmer, W. | A Unification Algorithm for Second Order Monadic Terms [BibTeX] |
1988 | Annals of Pure and Applied Logic Vol. 39, pp. 131-174 |
article | DOI |

BibTeX:
@article{Far:88, author = {W. Farmer}, title = {A Unification Algorithm for Second Order Monadic Terms}, journal = {Annals of Pure and Applied Logic}, year = {1988}, volume = {39}, pages = {131--174}, note = {http://dx.doi.org/10.1016/0168-0072(88)90015-2Electronic Edition}, doi = {http://dx.doi.org/10.1016/0168-0072(88)90015-2} } |
|||||

Felty, A. & Howe, D. | Generalization and Reuse of Tactic Proofs [BibTeX] |
1994 | Vol. 8225th International Conference on Logic Programming and Automated Reasoning, pp. 1-15 |
inproceedings | |

BibTeX:
@inproceedings{FM:94, author = {A. Felty and D. Howe}, title = {Generalization and Reuse of Tactic Proofs}, booktitle = {5th International Conference on Logic Programming and Automated Reasoning}, publisher = {Springer-Verlag }, year = {1994}, volume = {822}, pages = {1--15}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1064Electronic Edition} } |
|||||

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} } |
|||||

Fraenkel, A. | The notion "definite" and the independence of axiom of choice [BibTeX] |
1922 | English translation in From Frege to Gödel, a Source Book in Mathematical Logic (J. van Heijenoort, Editor), Harvard |
misc | |

BibTeX:
@misc{Fra:22, author = {A. Fraenkel}, title = {The notion "definite" and the independence of axiom of choice}, year = {1922} } |
|||||

Frege, G. | Grundgesetze der Aritmetik, begriffsschriftlich abgeleitet, Vol. 2 [BibTeX] |
1904 | book | ||

BibTeX:
@book{Fre:03, author = {G. Frege}, title = {Grundgesetze der Aritmetik, begriffsschriftlich abgeleitet, Vol. 2}, publisher = {Jena}, year = {1904} } |
|||||

Frege, G. | Grundgesetze der Aritmetik, begriffsschriftlich abgeleitet, Vol. 1 [BibTeX] |
1893 | book | ||

BibTeX:
@book{Fre:93, author = {G. Frege}, title = {Grundgesetze der Aritmetik, begriffsschriftlich abgeleitet, Vol. 1}, publisher = {Jena}, year = {1893} } |
|||||

Frege, G. | Begriffsschrift, eine der Arithmetischen Nachgebildete Formelsprache des Reinen Denkens [BibTeX] |
1879 | book | ||

BibTeX:
@book{Fre:79, author = {G. Frege}, title = {Begriffsschrift, eine der Arithmetischen Nachgebildete Formelsprache des Reinen Denkens}, publisher = {Halle}, year = {1879}, note = {English translation in |
|||||

Friedman, H. | Equality between Functionals. [BibTeX] |
1975 | Vol. 453Symposium on Logic Held at Boston, 1972-73, pp. 22-37 |
inproceedings | |

BibTeX:
@inproceedings{Fri:75, author = {H. Friedman}, title = {Equality between Functionals.}, booktitle = {Symposium on Logic Held at Boston, 1972-73}, publisher = {Springer-Verlag}, year = {1975}, volume = {453}, pages = {22--37} } |
|||||

Gabbay, M. & Pitts, A.M. | A New Approach to Abstract Syntax Involving Binders [BibTeX] |
1999 | LICS, pp. 214-224 | inproceedings | DOI |

BibTeX:
@inproceedings{GP:99, author = {Murdoch Gabbay and Andrew M. Pitts}, title = {A New Approach to Abstract Syntax Involving Binders}, booktitle = {LICS}, year = {1999}, pages = {214-224}, doi = {http://computer.org/conferen/proceed/lics/0158/01580214abs.htm} } |
|||||

Gabbay, M.J. | FM-HOL, a higher-order theory of names [BibTeX] |
2002 | 35 Years of Automath | inproceedings | |

BibTeX:
@inproceedings{MG:02, author = {Murdoch J. Gabbay}, title = {FM-HOL, a higher-order theory of names}, booktitle = {35 Years of Automath}, year = {2002} } |
|||||

Gabbay, M.J. | A Theory of Inductive Definitions with $-Equivalence [BibTeX] |
2000 | School: Cambridge University, UK |
phdthesis | |

BibTeX:
@phdthesis{MG:00, author = {Murdoch J. Gabbay}, title = {A Theory of Inductive Definitions with $-Equivalence}, school = {Cambridge University, UK}, year = {2000} } |
|||||

Gabbay, M.J. & Pitts, A.M. | A New Approach to Abstract Syntax with Variable Binding [BibTeX] |
2002 | Formal Aspects of Computing Vol. 13(3-5), pp. 341-363 |
article | |

BibTeX:
@article{MGAP:02, author = {Murdoch J. Gabbay and Andrew M. Pitts}, title = {A New Approach to Abstract Syntax with Variable Binding}, journal = {Formal Aspects of Computing}, year = {2002}, volume = {13}, number = {3--5}, pages = {341--363} } |
|||||

Gibbons, J. | Generic downwards accumulations [BibTeX] |
2000 | Science of Computer Programming Vol. 37(1-3), pp. 37 -65 |
article | |

BibTeX:
@article{JG:00, author = {Jeremy Gibbons}, title = {Generic downwards accumulations}, journal = {Science of Computer Programming}, year = {2000}, volume = {37}, number = {1-3}, pages = {37 --65} } |
|||||

Gibbons, J., Hutton, G. & Altenkirch, T. | When is a Function a Fold or an Unfold? [BibTeX] |
2001 | Vol. 44(1)Proc. of 4th Workshop on Coalgebraic Methods in Computer Science, CMCS'01 (Genova, Italy, 6--7 Apr. 2001) |
incollection | URL |

BibTeX:
@incollection{KGGHTA:01, author = {Jeremy Gibbons and Graham Hutton and Thorsten Altenkirch}, title = {When is a Function a Fold or an Unfold?}, booktitle = {Proc. of 4th Workshop on Coalgebraic Methods in Computer Science, CMCS'01 (Genova, Italy, 6--7 Apr. 2001)}, publisher = {Elsevier}, year = {2001}, volume = {44(1)}, url = {http://www.cs.nott.ac.uk/~gmh/when.ps} } |
|||||

Gil, J. | Subtyping arithmetical types. [BibTeX] |
2001 | SIGPLAN Vol. 36(3)Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 276-289 |
article | DOI |

BibTeX:
@article{Gil:01, author = {J. Gil}, title = {Subtyping arithmetical types.}, booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, journal = {SIGPLAN}, publisher = {ACM Press}, year = {2001}, volume = {36}, number = {3}, pages = {276-289}, note = {http://doi.acm.org/10.1145/360204.360232Electronic Edition}, doi = {http://doi.acm.org/10.1145/373243.360232} } |
|||||

Gil, J. & Zibin, Y. | Randomised algorithms for isomorphisms of simple types [BibTeX] |
2007 | Mathematical Structures in Computer Science Vol. 17(3), pp. 565-584 |
article | URL |

BibTeX:
@article{JGYZ:07, author = {Joseph Gil and Yoav Zibin}, title = {Randomised algorithms for isomorphisms of simple types}, journal = {Mathematical Structures in Computer Science}, year = {2007}, volume = {17}, number = {3}, pages = {565--584}, url = {http://dx.doi.org/10.1017/S0960129507006068} } |
|||||

Gil, J. & Zibin, Y. | Efficient algorithms for isomorphisms of simple types [BibTeX] |
2005 | Mathematical Structures in Computer Science Vol. 15(5), pp. 917-957 |
article | URL |

BibTeX:
@article{JGYZ:05, author = {Joseph Gil and Yoav Zibin}, title = {Efficient algorithms for isomorphisms of simple types}, journal = {Mathematical Structures in Computer Science}, year = {2005}, volume = {15}, number = {5}, pages = {917--957}, url = {http://dx.doi.org/10.1017/S0960129505004913} } |
|||||

Gill, A.J., Launchbury, J. & Jones, S.L.P. | A Short Cut to Deforestation [BibTeX] |
1993 | FPCA, pp. 223-232 | inproceedings | |

BibTeX:
@inproceedings{AGJLSP:93, author = {Andrew J. Gill and John Launchbury and Simon L. Peyton Jones}, title = {A Short Cut to Deforestation}, booktitle = {FPCA}, year = {1993}, pages = {223-232} } |
|||||

Goldfard, W. | The undecidability of the second order unification problem [BibTeX] |
1981 | Theoretical Computer Science Vol. 13, pp. 225-230 |
article | DOI |

BibTeX:
@article{Gol:81, author = {W. Goldfard}, title = {The undecidability of the second order unification problem}, journal = {Theoretical Computer Science}, year = {1981}, volume = {13}, pages = {225--230}, note = {http://dx.doi.org/10.1016/0304-3975(81)90040-2Electronic Edition}, doi = {http://dx.doi.org/10.1016/0304-3975(81)90040-2} } |
|||||

de Groote, P. | Linear Higher-Order Matching Is NP-Complete [BibTeX] |
2000 | Vol. 1833RTA '00: Proceedings of the 11th International Conference on Rewriting Techniques and Applications, pp. 127-140 |
inproceedings | |

BibTeX:
@inproceedings{Gro:00, author = {P. de Groote}, title = {Linear Higher-Order Matching Is NP-Complete}, booktitle = {RTA '00: Proceedings of the 11th International Conference on Rewriting Techniques and Applications}, publisher = {Springer-Verlag}, year = {2000}, volume = {1833}, pages = {127--140}, note = {http://portal.acm.org/citation.cfm?id=647199.718705Electronic Edition} } |
|||||

de Groote, P. | Proof-Search in Implicative Linear Logic as a Matching Problem [BibTeX] |
2000 | Lecture Notes in Computer Science Vol. 1955, pp. 257-?? |
article | URL |

BibTeX:
@article{PG:00, author = {Philippe de Groote}, title = {Proof-Search in Implicative Linear Logic as a Matching Problem}, journal = {Lecture Notes in Computer Science}, year = {2000}, volume = {1955}, pages = {257--??}, url = {http://link.springer-ny.com/link/service/series/0558/bibs/1955/19550257.htm; http://link.springer-ny.com/link/service/series/0558/papers/1955/19550257.pdf} } |
|||||

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} } |
|||||

Gurevič, R. | Equational Theory of Positive Numbers with Exponentiation [BibTeX] |
1985 | Vol. 84(1)Proceedings of the American Mathematical Society, pp. 135-141 |
inproceedings | URL |

BibTeX:
@inproceedings{Gu:85, author = {R. Gurevič}, title = {Equational Theory of Positive Numbers with Exponentiation}, booktitle = {Proceedings of the American Mathematical Society}, year = {1985}, volume = {84}, number = {1}, pages = {135--141}, note = {http://www.jstor.org/stable/2044966Electronic Edition}, url = {http://www.jstor.org/stable/2044966} } |
|||||

Gurevič, R. | Equational theory of positive numbers with exponentiation is not finitely axiomatizable [BibTeX] |
1990 | Annals of Pure and Applied Logic Vol. 49(1), pp. 1-30 |
article | DOI |

BibTeX:
@article{Gur:90, author = {R. Gurevič}, title = {Equational theory of positive numbers with exponentiation is not finitely axiomatizable}, journal = {Annals of Pure and Applied Logic}, year = {1990}, volume = {49}, number = {1}, pages = {1--30}, note = {http://dx.doi.org/10.1016/0168-0072(90)90049-8Electronic Edition }, doi = {http://dx.doi.org/10.1016/0168-0072(90)90049-8} } |
|||||

Harrison, R. & Glass, C.A. | Dynamic Programming in a Pure Functional Language [BibTeX] |
1993 | Proceedings of the ACM/SIGAPP Symposium on Applied Computing, pp. 179-186 |
inproceedings | URL |

BibTeX:
@inproceedings{RHCG:93, author = {Rachel Harrison and Celia A. Glass}, title = {Dynamic Programming in a Pure Functional Language}, booktitle = {Proceedings of the ACM/SIGAPP Symposium on Applied |
|||||

van Heijenoort, J. | From Frege to Gödel [BibTeX] |
1967 | book | ||

BibTeX:
@book{vHe:67, author = {J. van Heijenoort}, title = {From Frege to Gödel}, publisher = {Harvard University Press}, year = {1967} } |
|||||

Herbrand, J. | Recherches sur la théorie de la démonstration [BibTeX] |
1930 | (Th{\`e}se de doctorat)School: Université de Paris |
phdthesis | |

BibTeX:
@phdthesis{Her:30, author = {J. Herbrand}, title = {Recherches sur la théorie de la démonstration}, school = {Université de Paris}, year = {1930}, number = {Thèse de doctorat} } |
|||||

Hilbert, D. | The Problems of Mathematics [BibTeX] |
1900 | Second International Congress of Mathematicians in Paris | other | URL |

BibTeX:
@other{Hil:00, author = {D. Hilbert}, title = {The Problems of Mathematics}, year = {1900}, note = {http://en.wikipedia.org/wiki/Hilbert's_problemsElectronic Edition}, url = {http://en.wikipedia.org/wiki/Hilbert's_problems} } |
|||||

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} } |
|||||

Hu, Z., Iwasaki, H., Takeichi, M. & Takano, A. | Tupling Calculation Eliminates Multiple Data Traversals [BibTeX] |
1997 | ICFP, pp. 164-175 | inproceedings | |

BibTeX:
@inproceedings{ZHHIMTAT:97, author = {Zhenjiang Hu and Hideya Iwasaki and Masato Takeichi and Akihiko Takano}, title = {Tupling Calculation Eliminates Multiple Data Traversals}, booktitle = {ICFP}, year = {1997}, pages = {164-175} } |
|||||

Huet, G. | Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems [BibTeX] |
1980 | Journal of the Association for Computing Machinery Vol. 27(4), pp. 797-821 |
article | |

BibTeX:
@article{GH:80, author = {Gérard Huet}, title = {Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems}, journal = {Journal of the Association for Computing Machinery}, year = {1980}, volume = {27}, number = {4}, pages = {797--821}, note = {Preliminary version in it Proceedings, 18th IEEE Symposium on Foundations of Computer Science, IEEE, 1977, pages 30--45} } |
|||||

Huet, G. | Resolution d'Equations dans les langages d'ordre 1, 2, $ [BibTeX] |
1976 | School: Université de Paris VII |
phdthesis | |

BibTeX:
@phdthesis{Hue:76, author = {G. Huet}, title = {Resolution d'Equations dans les langages d'ordre 1, 2, $}, school = {Université de Paris VII}, year = {1976} } |
|||||

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} } |
|||||

Huet, G. | The Undecidability of Unification in Third Order Logics [BibTeX] |
1973 | Information and Control Vol. 22, pp. 257-267 |
article | DOI |

BibTeX:
@article{Hue:73, author = {G. Huet}, title = {The Undecidability of Unification in Third Order Logics}, journal = {Information and Control}, year = {1973}, volume = {22}, pages = {257--267}, note = {http://dx.doi.org/10.1016/S0019-9958(73)90301-XElectronic Edition}, doi = {http://dx.doi.org/10.1016/S0019-9958(73)90301-X} } |
|||||

Huet, G. | Constrained Resolution: A Complete Method for Higher Order Logic [BibTeX] |
1972 | School: Case Western Reserve University |
phdthesis | |

BibTeX:
@phdthesis{Hue:72, author = {G. Huet}, title = {Constrained Resolution: A Complete Method for Higher Order Logic}, school = {Case Western Reserve University}, year = {1972}, note = {http://portal.acm.org/citation.cfm?id=906084Electronic Edition} } |
|||||

Huet, G. & Lang, B. | Proving and applying program transformations expressed with second-order patterns [BibTeX] |
1978 | Acta Informatica. Vol. 11(1), pp. 31-55 |
article | DOI |

BibTeX:
@article{HL:78, author = {G. Huet and B. Lang}, title = {Proving and applying program transformations expressed with second-order patterns}, journal = {Acta Informatica.}, publisher = {Springer-Verlag}, year = {1978}, volume = {11}, number = {1}, pages = {31--55}, note = {http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/BF00264598Electronic Edition}, doi = {http://www.springerlink.com/openurl.asp?genre=article\&id=doi:10.1007/BF00264598} } |
|||||

Huet, Gé.P. | Higher Order Unification 30 Years Later [BibTeX] |
2002 | TPHOLs, pp. 3-12 | inproceedings | URL |

BibTeX:
@inproceedings{GH:02, author = {Gérard P. Huet}, title = {Higher Order Unification 30 Years Later}, booktitle = {TPHOLs}, year = {2002}, pages = {3-12}, url = {http://link.springer.de/link/service/series/0558/bibs/2410/24100003.htm} } |
|||||

Hughes, R.J.M. | Why Functional Programming Matters [BibTeX] |
1989 | The Computer Journal Vol. 32(2), pp. 98-107 |
article | URL |

BibTeX:
@article{Hug:89, author = {R. J. M. Hughes}, title = {Why Functional Programming Matters}, journal = {The Computer Journal}, year = {1989}, volume = {32}, number = {2}, pages = {98--107}, note = {http://www.math.chalmers.se/~rjmh/Papers/whyfp.htmlElectronic Edition}, url = {http://www.math.chalmers.se/~rjmh/Papers/whyfp.html} } |
|||||

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} } |
|||||

INRIA | The Objective Caml system [BibTeX] |
Since 1985 | other | ||

BibTeX:
@other{Ocaml, author = {INRIA}, title = {The Objective Caml system}, year = {Since 1985}, note = { http://caml.inria.fr/index.en.htmlWebsite} } |
|||||

Jansson, P. & Jeuring, J.T. | Polytypic Data Conversion Programs [BibTeX] |
2002 | misc | URL | |

BibTeX:
@misc{PJJJ:02, author = {Patrik Jansson and Johan Theodoor Jeuring}, title = {Polytypic Data Conversion Programs}, year = {2002}, url = {http://www.library.uu.nl/digiarchief/dip/dispute/2002-0308-100819/2001-34.pdf} } |
|||||

Jay, C.B. & Ghani, N. | The Virtues of Eta-expansion [BibTeX] |
1995 | Journal of Functional Programming Vol. 5(2), pp. 135-154 |
article | |

BibTeX:
@article{JG:95, author = {C. B. Jay and N. Ghani}, title = {The Virtues of Eta-expansion}, journal = {Journal of Functional Programming}, year = {1995}, volume = {5}, number = {2}, pages = {135--154}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.613Electronic Edition} } |
|||||

Jenner, B., Köbler, J., McKenzie, P. & Torán, J. | Corrigendum to "Completeness results for graph isomorphism" [J. Comput. System Sci. 66(2003) 549-566] [BibTeX] |
2006 | J. Comput. Syst. Sci Vol. 72(4), pp. 783 |
article | URL |

BibTeX:
@article{BJJKPMJT:06, author = {Birgit Jenner and Johannes Köbler and Pierre McKenzie and Jacobo Torán}, title = {Corrigendum to "Completeness results for graph isomorphism" [J. Comput. System Sci. 66(2003) 549-566]}, journal = {J. Comput. Syst. Sci}, year = {2006}, volume = {72}, number = {4}, pages = {783}, url = {http://dx.doi.org/10.1016/j.jcss.2005.11.002} } |
|||||

Jenner, B. & Lange, K. | Tree Isomorphism and Some Other Complete Problems for Deterministic Logspace | 1997 | misc | URL | |

Abstract: Several new tree problems are shown complete for deterministic logarithmic space. These include the tree centroid problem and the tree isomorphism problem, which thus becomes the first isomorphism problem of a combinatorial nature shown complete for a fundamental resource-based complexity class. The crucial role of the input representation of trees, as edge lists or as bracketed expressions, on the hardness of tree problems, is also discussed. R'esum'e Nous d'emontrons que certains probl`emes concernant des arbres sont complets pour la classe de complexit'e L form'ee des langages reconnus en espace logarithmique. Un de ces probl`emes est celui de d'eterminer si deux arbres sont isomorphes. Il s'agit donc dans ce cas d'un premier probl`eme d'isomorphisme `a caract`ere combinatoire dont on puisse d'emontrer la compl'etude pour une classe de complexit'e robuste d'efinie par bornes de ressources. Un autre probl`eme dont nous prouvons la L-compl'etude est celui de d'eterminer si le retrai... |
|||||

BibTeX:
@misc{BJKL:97, author = {Birgit Jenner and Klaus-jorn Lange}, title = {Tree Isomorphism and Some Other Complete Problems for Deterministic Logspace}, year = {1997}, url = {http://citeseer.ist.psu.edu/125009.html; http://www.iro.umontreal.ca/~mckenzie/jelamc97.ps} } |
|||||

Jenner, B., McKenzie, P. & Torán, J. | A Note on the Hardness of Tree Isomorphism [BibTeX] |
1998 | Proceedings of the 13th Annual IEEE Conference on Computational Complexity, pp. 101-105 | inproceedings | |

BibTeX:
@inproceedings{BJPMJT:98, author = {Birgit Jenner and Pierre McKenzie and Jacobo Torán}, title = {A Note on the Hardness of Tree Isomorphism}, booktitle = {Proceedings of the 13th Annual IEEE Conference on Computational Complexity}, publisher = {IEEE Computer Society Press}, year = {1998}, pages = {101--105} } |
|||||

Jha, S., Palsberg, J. & Zhao, T. | Efficient Type Matching [BibTeX] |
2002 | Lecture Notes in Computer Science Vol. 2303, pp. 187-?? |
article | URL |

BibTeX:
@article{SJJPTZ:02, author = {Somesh Jha and Jens Palsberg and Tian Zhao}, title = {Efficient Type Matching}, journal = {Lecture Notes in Computer Science}, year = {2002}, volume = {2303}, pages = {187--??}, url = {http://link.springer-ny.com/link/service/series/0558/bibs/2303/23030187.htm; http://link.springer-ny.com/link/service/series/0558/papers/2303/23030187.pdf} } |
|||||

Johann, P. | On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi [BibTeX] |
2005 | Mathematical Structures in Computer Science Vol. 15(2), pp. 201-229 |
article | URL |

BibTeX:
@article{PJ:05, author = {Patricia Johann}, title = {On proving the correctness of program transformations based on free theorems for higher-order polymorphic calculi}, journal = {Mathematical Structures in Computer Science}, year = {2005}, volume = {15}, number = {2}, pages = {201--229}, url = {http://dx.doi.org/10.1017/S0960129504004578} } |
|||||

Johann, P. & Launchbury, J. | Warm Fusion for Masses: Detailing Virtual Data Structure Elimination in Fully Recursive Languages [BibTeX] |
1998 | unpublished | URL | |

BibTeX:
@unpublished{PJJL:98, author = {Patricia Johann and John Launchbury}, title = {Warm Fusion for Masses: Detailing Virtual Data Structure Elimination in Fully Recursive Languages}, year = {1998}, note = {Unpublished draft}, url = {ftp://ftp.cse.ogi.edu/pub/pacsoft/2final_report/wfpaper.ps} } |
|||||

Jones, S.L.P. | Compiling Haskell by Program Transformation: A Report from the Trenches [BibTeX] |
1996 | Vol. 1058Programming Languages and Systems---ESOP'96, pp. 18-44 |
inproceedings | |

BibTeX:
@inproceedings{SlP:96, author = {Simon L. Peyton Jones}, title = {Compiling Haskell by Program Transformation: A Report from the Trenches}, booktitle = {Programming Languages and Systems---ESOP'96}, publisher = {Springer-Verlag}, year = {1996}, volume = {1058}, pages = {18--44} } |
|||||

Jones, S.L.P. & Santos, A.L.M. | A transformation-based optimiser for~Haskell [BibTeX] |
1998 | Science of Computer Programming Vol. 32(1-3), pp. 3-47 |
article | |

BibTeX:
@article{SPJAS:98, author = {Simon L. Peyton Jones and André L. M. Santos}, title = {A transformation-based optimiser for~Haskell}, journal = {Science of Computer Programming}, year = {1998}, volume = {32}, number = {1--3}, pages = {3--47} } |
|||||

Jones, S.P., Tolmach, A. & Hoare, T. | Playing by the Rules: Rewriting as a practical optimisation technique in GHC | 2001 | misc | URL | |

Abstract: We describe a facility for improving optimization of Haskell programs using rewrite rules. Library authors can use rules to express domain-specic optimizations that the compiler cannot discover for itself. The compiler can also generate rules internally to propagate information obtained from automated analyses. The rewrite mechanism is fully implemented in the released Glasgow Haskell Compiler. Our system is very simple, but can be eective in optimizing real programs. We describe two practical applications involving short-cut deforestation, for lists and for rose trees, and document substantial performance improvements on a range of programs. This paper has been submitted to ICFP 2001. 1 |
|||||

BibTeX:
@misc{SPATTH:01, author = {Simon Peyton Jones and Andrew Tolmach and Tony Hoare}, title = {Playing by the Rules: Rewriting as a practical optimisation technique in GHC}, year = {2001}, url = {http://citeseer.ist.psu.edu/464981.html} } |
|||||

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} } |
|||||

Kleene, S.C. & Rosser, J.B. | The inconsistency of certain formal logics [BibTeX] |
1935 | The Annals of Mathematics, Second Series Vol. 36, pp. 630-636 |
article | URL |

BibTeX:
@article{KR:35, author = {S. C. Kleene and J. B. Rosser}, title = {The inconsistency of certain formal logics}, journal = {The Annals of Mathematics, Second Series}, year = {1935}, volume = {36}, pages = {630--636}, note = {http://www.jstor.org/stable/1968646Electronic Edition}, url = {http://www.jstor.org/stable/1968646} } |
|||||

Knight, K. | Unification: A Multidisciplinary Survey [BibTeX] |
1989 | ACM Computing Surveys Vol. 21(1), pp. 93-124 |
article | |

BibTeX:
@article{KN:89, author = {K. Knight}, title = {Unification: A Multidisciplinary Survey}, journal = {ACM Computing Surveys}, year = {1989}, volume = {21}, number = {1}, pages = {93--124} } |
|||||

Kolbe, T. & Walther, C. | Proof Analysis, Generalization, and Reuse [BibTeX] |
1998 | Vol. Volume {II}, Systems and Implementation TechniquesAutomated Deduction: A Basis for Applications. |
incollection | URL |

BibTeX:
@incollection{KW:98, author = {T. Kolbe and C. Walther}, title = {Proof Analysis, Generalization, and Reuse}, booktitle = {Automated Deduction: A Basis for Applications.}, publisher = {Kluwer Academic Publishers}, year = {1998}, volume = {Volume II, Systems and Implementation Techniques}, note = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Proof_Analysis_Generalization_and_Reuse.psElectronic Edition }, url = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Proof_Analysis_Generalization_and_Reuse.ps} } |
|||||

Kolbe, T. & Walther, C. | Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs [BibTeX] |
1995 | Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, pp. 190-195 | inproceedings | URL |

BibTeX:
@inproceedings{KT:95, author = {T. Kolbe and C. Walther}, title = {Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs}, booktitle = {Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence}, publisher = {Morgan Kaufmann}, year = {1995}, pages = {190--195}, note = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Second-Order-Matching-mod-Eval-IJCAI-1995.pdfElectronic Edition}, url = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Second-Order-Matching-mod-Eval-IJCAI-1995.pdf} } |
|||||

Kozen, D. | The Design and Analysis of Algorithms [BibTeX] |
1992 | book | URL | |

BibTeX:
@book{Koz:92, author = {D. Kozen}, title = {The Design and Analysis of Algorithms}, publisher = {Springer}, year = {1992}, note = {http://books.google.com/books?id=L_AMnf9UF9QC&dq=The+Design+and+Analysis+of+Algorithms&source=gbs_summary_s&cad=0Electronic Edition}, url = {http://books.google.com/books?id=L_AMnf9UF9QC&dq=The+Design+and+Analysis+of+Algorithms&source=gbs_summary_s&cad=0} } |
|||||

Kuncak, V. & Rinard, M. | Structural Subtyping of Non-Recursive Types is Decidable [BibTeX] |
2003 | Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science, pp. 96-107 | inproceedings | |

BibTeX:
@inproceedings{KR:03, author = {V. Kuncak and M. Rinard}, title = {Structural Subtyping of Non-Recursive Types is Decidable}, booktitle = {Proceedings of the Eighteenth Annual IEEE Symp. on Logic in Computer Science}, publisher = {IEEE Computer Society Press}, year = {2003}, pages = {96--107}, note = {http://citeseer.ist.psu.edu/kuncak03structural.htmlElectronic Edition} } |
|||||

L. Paulson, T.N. | The ISABELLE theorem prover [BibTeX] |
Since 1989 | other | URL | |

BibTeX:
@other{ISABELLE, author = {L. Paulson, T. Nipkow}, title = {The ISABELLE theorem prover}, year = {Since 1989}, note = {http://www.cl.cam.ac.uk/Research/HVG/Isabelle/Website}, url = {http://www.cl.cam.ac.uk/Research/HVG/Isabelle/} } |
|||||

Laan, T. | A formalization of the Ramified Type Theory [BibTeX] |
1994 | techreport | ||

BibTeX:
@techreport{La:94, author = {T. Laan}, title = {A formalization of the Ramified Type Theory}, year = {1994}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.8847Electronic Edition} } |
|||||

Lambek, J. & Scott, P.J. | Introduction to higher order categorical logic [BibTeX] |
1986 | (7) | book | |

BibTeX:
@book{LS:86, author = {J. Lambek and P. J. Scott}, title = {Introduction to higher order categorical logic}, publisher = {Cambridge University Press}, year = {1986}, number = {7}, note = { http://www.andrew.cmu.edu/user/cebrown/notes/lambekscott.htmlElectronic Edition} } |
|||||

Landauer, R. | Irreversibility and heat generation in the computing process [BibTeX] |
1961 | IBM-Journal of Research and Development Vol. 3(1/2), pp. 183-192 |
article | URL |

BibTeX:
@article{Lan:61, author = {R. Landauer}, title = {Irreversibility and heat generation in the computing process}, journal = {IBM-Journal of Research and Development}, year = {1961}, volume = {3}, number = {1/2}, pages = {183--192}, note = {http://www.research.ibm.com/journal/rd/441/landauerii.pdfElectronic Edition}, url = {http://www.research.ibm.com/journal/rd/441/landauerii.pdf} } |
|||||

Lataillade, J. | Curry-style type isomorphisms and game semantics [BibTeX] |
2007 | unpublished | URL | |

BibTeX:
@unpublished{Lat:07, author = {Lataillade, Joachim}, title = {Curry-style type isomorphisms and game semantics}, year = {2007}, note = {http://arxiv.org/abs/0705.4228Electronic Edition}, url = {http://arxiv.org/abs/0705.4228} } |
|||||

Lataillade, J.D. | Second-Order Type Isomorphisms Through Game Semantics [BibTeX] |
2007 | CoRR Vol. abs/0705.4226 |
article | URL |

BibTeX:
@article{JdL:07b, author = {Joachim De Lataillade}, title = {Second-Order Type Isomorphisms Through Game Semantics}, journal = {CoRR}, year = {2007}, volume = {abs/0705.4226}, note = {informal publication}, url = {http://arxiv.org/abs/0705.4226} } |
|||||

Launchbury, J. & Sheard, T. | Warm Fusion: Deriving Build-Cata's from Recursive Definitions [BibTeX] |
1995 | FPCA, pp. 314-323 | inproceedings | |

BibTeX:
@inproceedings{JLTS:95, author = {John Launchbury and Tim Sheard}, title = {Warm Fusion: Deriving Build-Cata's from Recursive Definitions}, booktitle = {FPCA}, year = {1995}, pages = {314-323} } |
|||||

Laurent, O. | Classical isomorphisms of types [BibTeX] |
2005 | Mathematical Structures in Computer Science Vol. 15, pp. 969-1004 |
article | DOI |

BibTeX:
@article{Lau:05, author = {Laurent, Olivier}, title = {Classical isomorphisms of types}, journal = {Mathematical Structures in Computer Science}, year = {2005}, volume = {15}, pages = {969-1004}, note = {http://dx.doi.org/10.1017/S0960129505004895Electronic Edition}, doi = {http://dx.doi.org/10.1017/S0960129505004895} } |
|||||

Lescanne, P. & Rouyer-Degli, J. | Explicit Substitutions with de Bruijn's Levels [BibTeX] |
1995 | RTA, pp. 294-308 | inproceedings | |

BibTeX:
@inproceedings{PLJRD:95, author = {Pierre Lescanne and Jocelyne Rouyer-Degli}, title = {Explicit Substitutions with de Bruijn's Levels}, booktitle = {RTA}, year = {1995}, pages = {294-308} } |
|||||

Levy, J. | Decidable and Undecidable Second-Order Unification Problems [BibTeX] |
1998 | Lecture Notes in Computer Science Vol. 1379, pp. 47-?? |
article | URL |

BibTeX:
@article{JL:98, author = {Jordi Levy}, title = {Decidable and Undecidable Second-Order Unification Problems}, journal = {Lecture Notes in Computer Science}, year = {1998}, volume = {1379}, pages = {47--??}, url = {http://link.springer-ny.com/link/service/series/0558/bibs/1379/13790047.htm} } |
|||||

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. | Higher Order $ Matching is Undecidable [BibTeX] |
2003 | Logic Journal of the IGPL Vol. 11(1), pp. 51-68 |
article | DOI |

BibTeX:
@article{Lo:03, author = {R. Loader}, title = {Higher Order $ Matching is Undecidable}, journal = {Logic Journal of the IGPL}, year = {2003}, volume = {11}, number = {1}, pages = {51--68}, note = {http://dx.doi.org/10.1093/jigpal/11.1.51Electronic Edition}, doi = {http://dx.doi.org/10.1093/jigpal/11.1.51} } |
|||||

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} } |
|||||

Lucchesi, C.L. | The undecidability of the Unification Problem for Third Order languages [BibTeX] |
1972 | School: University Waterloo |
techreport | |

BibTeX:
@techreport{Luc:72, author = {C. L. Lucchesi}, title = {The undecidability of the Unification Problem for Third Order languages}, school = {University Waterloo}, year = {1972}, note = {Report CSRR 2059, } } |
|||||

Luo, Z. | Coercive Subtyping [BibTeX] |
1999 | Journal of Logic and Computation Vol. 9(1), pp. 105-130 |
article | DOI URL |

BibTeX:
@article{Luo:98, author = {Z. Luo}, title = {Coercive Subtyping}, journal = {Journal of Logic and Computation}, year = {1999}, volume = {9}, number = {1}, pages = {105--130}, note = {http://www.dur.ac.uk/CARG/papers/JLC98.ps.gzElectronic Edition}, url = {http://www.dur.ac.uk/CARG/papers/JLC98.ps.gz}, doi = {http://dx.doi.org/10.1093/logcom/9.1.105} } |
|||||

Magaud, N. & Bertot, Y. | Changing Data Structures in Type Theory: A Study of Natural Numbers [BibTeX] |
2000 | Lecture Notes in Computer Science Vol. 2277TYPES, International Workshop on Types for Proofs and Programs, pp. 181 - 196 |
inproceedings | |

BibTeX:
@inproceedings{MB:02, author = {N. Magaud and Y. Bertot}, title = {Changing Data Structures in Type Theory: A Study of Natural Numbers}, booktitle = {TYPES, International Workshop on Types for Proofs and Programs}, journal = {Lecture Notes in Computer Science}, publisher = {Springer Verlag}, year = {2000}, volume = {2277}, pages = {181 - 196}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.3073Electronic Edition} } |
|||||

Maroney, O.J.E. | Are all reversible computations tidy? [BibTeX] |
2004 | unpublished | URL | |

BibTeX:
@unpublished{Mar:04, author = {O. J. E. Maroney}, title = {Are all reversible computations tidy?}, year = {2004}, note = {http://arxiv.org/abs/quant-ph/0403079Electronic Edition}, url = {http://arxiv.org/abs/quant-ph/0403079} } |
|||||

Martelli, A. & Montanari, U. | An Efficient Unification Algorithm [BibTeX] |
1982 | AMC Transactions on Programming Languages and Systems Vol. 4(2), pp. 258-282 |
article | DOI |

BibTeX:
@article{MM:82, author = {A. Martelli and U. Montanari}, title = {An Efficient Unification Algorithm}, journal = {AMC Transactions on Programming Languages and Systems}, publisher = {Association of Computing Machinery Press}, year = {1982}, volume = {4}, number = {2}, pages = {258--282}, note = {http://doi.acm.org/10.1145/357162.357169Electronic Edition}, doi = {http://doi.acm.org/10.1145/357162.357169} } |
|||||

Martin, C. | Axiomatic bases for equational theories of natural numbers [BibTeX] |
1972 | Notices of American Mathematical Society Vol. 19(8), pp. 778 |
article | |

BibTeX:
@article{Mar:70, author = {C. Martin}, title = {Axiomatic bases for equational theories of natural numbers}, journal = {Notices of American Mathematical Society}, year = {1972}, volume = {19}, number = {8}, pages = {778} } |
|||||

Martin, U. & Nipkow, T. | Unification in Boolean rings [BibTeX] |
1988 | Journal of Automated Reasoning Vol. 4, pp. 381-396 |
article | |

BibTeX:
@article{UMTN:88, author = {Ursula Martin and Tobias Nipkow}, title = {Unification in Boolean rings}, journal = {Journal of Automated Reasoning}, year = {1988}, volume = {4}, pages = {381--396} } |
|||||

Matiyacevich, Y. | Enumerable sets are Diophantine [BibTeX] |
1970 | Soviet Mathematical Vol. 11, pp. 354-357 |
article | URL |

BibTeX:
@article{Mat:01, author = {Y. Matiyacevich}, title = {Enumerable sets are Diophantine}, journal = {Soviet Mathematical}, year = {1970}, volume = {11}, pages = {354--357}, note = {http://www.jstor.org/stable/2272763Electronic Edition}, url = {http://www.jstor.org/stable/2272763} } |
|||||

McAdam, B. | Repairing Type Errors in Functional Programs [BibTeX] |
2002 | School: The University of Edinburgh |
phdthesis | |

BibTeX:
@phdthesis{Mc:02, author = {B. McAdam}, title = {Repairing Type Errors in Functional Programs}, school = {The University of Edinburgh}, year = {2002}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.3740Electronic 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 } } |
|||||

Miller, D., Nadathur, G., Pfenning, F. & Scedrov, A. | Uniform Proofs as a Foundation for Logic Programming [BibTeX] |
1991 | Annals of Pure and Applied Logic Vol. 51(1-2), pp. 125-157 |
article | |

BibTeX:
@article{DM:91a, author = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov}, title = {Uniform Proofs as a Foundation for Logic Programming}, journal = {Annals of Pure and Applied Logic}, year = {1991}, volume = {51}, number = {1--2}, pages = {125--157} } |
|||||

Mitra, S. & Dershowitz, N. | Matching and Unification in Rewrite Theories | 1997 | misc | URL | |

Abstract: "Semantic unification" is the process of generating a basis set of substitutions (of terms for variables) that makes two given terms equal in a specified theory. Semantic unification is an important component of some theorem provers. "Semantic matching," a simpler variant of unification, where the substitution is made in only one of the terms, has potential usage in programming language interpreters. Decidable matching is required for pattern application in patterndirected languages, while decidable unification is useful for theorem proving modulo an equational theory. In this paper we restrict ourselves to matching and unification problems in theories that can be presented as convergent rewrite systems, that is, finite sets of equations that compute unique output values when applied (from left-to-right) to input values. The new results presented here, together with existing results, provide a much finer characterization of decidable matching and unification than was available before. ... |
|||||

BibTeX:
@misc{SMND:97, author = {Subrata Mitra and Nachum Dershowitz}, title = {Matching and Unification in Rewrite Theories}, year = {1997}, url = {http://citeseer.ist.psu.edu/52607.html} } |
|||||

de Moor, O. & Sittampalam, G. | Higher-order matching for program transformation [BibTeX] |
2001 | Theoretical Compuer Science Vol. 269(1-2), pp. 135-162 |
article | |

BibTeX:
@article{OS:01, author = {O. de Moor and G. Sittampalam}, title = {Higher-order matching for program transformation}, journal = {Theoretical Compuer Science}, publisher = {Elsevier Science Publishers B.V. (North Holland)}, year = {2001}, volume = {269}, number = {1-2}, pages = {135--162}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.3784Electronic Edition} } |
|||||

Muntz, R.R., Yang, Y. & Chi, Y. | Mining Frequent Rooted Trees and Free Trees Using Canonical Forms [BibTeX] |
2003 | techreport | ||

BibTeX:
@techreport{MYC:03, author = {R. R. Muntz and Y. Yang and Y. Chi}, title = {Mining Frequent Rooted Trees and Free Trees Using Canonical Forms}, year = {2003}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.8143Electronic Edition} } |
|||||

Narendran, P. | Some Remarks On Second Order Unification [BibTeX] |
1989 | (89/356/18) | techreport | URL |

BibTeX:
@techreport{Nar:89, author = {P. Narendran}, title = {Some Remarks On Second Order Unification}, year = {1989}, number = {89/356/18}, note = {http://hdl.handle.net/1880/46585Electronic Edition}, url = {http://hdl.handle.net/1880/46585} } |
|||||

Narendran, P., Pfenning, F. & Statman, R. | On the Unification Problem for Cartesian Closed Categories [BibTeX] |
1997 | Journal of Symbolic Logic. Vol. 62(2), pp. 636-647 |
article | |

BibTeX:
@article{PNFPRS:97, author = {Paliath Narendran and Frank Pfenning and Richard Statman}, title = {On the Unification Problem for Cartesian Closed Categories}, journal = {Journal of Symbolic Logic.}, year = {1997}, volume = {62}, number = {2}, pages = {636-647} } |
|||||

Nipkow, T. | Functional Unification of Higher-Order Patterns [BibTeX] |
1993 | Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science, pp. 64-74 | inproceedings | URL |

BibTeX:
@inproceedings{Nip:93, author = {T. Nipkow}, title = {Functional Unification of Higher-Order Patterns}, booktitle = {Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science}, publisher = {IEEE Computer Society Press}, year = {1993}, pages = {64--74}, note = {http://www4.in.tum.de/~nipkow/pubs/lics93.htmlElectronic Edition}, url = {http://www4.informatik.tu-muenchen.de/~nipkow/pubs/lics93.html} } |
|||||

Nipkow, T. | Proof Transformations for Equational Theories [BibTeX] |
1990 | LICS, pp. 278-288 | inproceedings | |

BibTeX:
@inproceedings{TN:90, author = {Tobias Nipkow}, title = {Proof Transformations for Equational Theories}, booktitle = {LICS}, publisher = {IEEE Computer Society}, year = {1990}, pages = {278--288} } |
|||||

Otto, F., Narendran, P. & Dougherty, D.J. | Some Independence Results For Equational Unification [BibTeX] |
1995 | Vol. 914Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95), pp. 367-381 |
inproceedings | |

BibTeX:
@inproceedings{FOPNDD:95, author = {Friedrich Otto and Paliath Narendran and Daniel J. Dougherty}, title = {Some Independence Results For Equational Unification}, booktitle = {Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA-95)}, publisher = {Springer-Verlag}, year = {1995}, volume = {914}, pages = {367--381} } |
|||||

Padovani, V. | Decidability of fourth-order matching [BibTeX] |
2000 | Mathematical Structures in Computer Science Vol. 10, pp. 361-372 |
article | URL |

BibTeX:
@article{Pad:94, author = {V. Padovani}, title = {Decidability of fourth-order matching}, journal = {Mathematical Structures in Computer Science}, year = {2000}, volume = {10}, pages = {361--372}, note = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=44653Electronic Edition}, url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=44653} } |
|||||

Padovani, V. | Decidability of All Minimal Models [BibTeX] |
1996 | Lecture Notes in Computer Science Vol. 1158TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs, pp. 201-?? |
inproceedings | DOI |

BibTeX:
@inproceedings{Pad:96, author = {V. Padovani}, title = {Decidability of All Minimal Models}, booktitle = {TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs}, journal = {Lecture Notes in Computer Science}, publisher = {Springer Verlag}, year = {1996}, volume = {1158}, pages = {201--??}, note = {http://dx.doi.org/10.1007/3-540-61780-9_71Electronic Edition,}, doi = {http://dx.doi.org/10.1007/3-540-61780-9_71} } |
|||||

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} } |
|||||

Palsberg, J. & Zhao, T. | Efficient and Flexible Matching of Recursive Types | 2000 | misc | URL | |

Abstract: Equality and subtyping of recursive types have been studied in the 1990s by Amadio and Cardelli; Kozen, Palsberg, and Schwartzbach; Brandt and Henglein; and others. Potential applications include automatic generation of bridge code for multi-language systems and type-based retrieval of software modules from libraries. Auerbach, Barton, and Raghavachari advocate a highly exible combination of matching rules for which there, until now, are no ecient algorithmic techniques. In this paper, we present an ecient decision procedure for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types, as advocated by Auerbach et al. For two types of size at most n, our algorithm decides equality in O(n 2 ) time. The algorithm iteratively prunes a set of type pairs, and eventually it produces a set of pairs of equal types. In each iteration, the algorithm exploits a so-called coherence property of the set of type pairs produced in the... |
|||||

BibTeX:
@misc{JPTZ:00, author = {Jens Palsberg and Tian Zhao}, title = {Efficient and Flexible Matching of Recursive Types}, year = {2000}, url = {http://citeseer.ist.psu.edu/388882.html; http://www.cs.purdue.edu/homes/tzhao/isomorphism/lics00.ps} } |
|||||

Pardo, A. | Fusion of Monadic (Co)Recursive Programs [BibTeX] |
1998 | Informal Proc. of Wksh. on Generic Programming (WGP'98, Marstrand, Sweden, 18 June 1998) | incollection | URL |

BibTeX:
@incollection{AP:98, author = {Alberto Pardo}, title = {Fusion of Monadic (Co)Recursive Programs}, booktitle = {Informal Proc. of Wksh. on Generic Programming (WGP'98, Marstrand, Sweden, 18 June 1998)}, publisher = {Dept. of Computing Science, Chalmers Univ. of Techn., and Göteborg Univ.}, year = {1998}, note = {Electronic version available at http://wsinwp01.win.tue.nl:1234/WGPProceedings/}, url = {http://www.fing.edu.uy/~pardo/papers/wgp98.ps.gz} } |
|||||

Pfenning, F. & Elliot, C. | Higher-Order Abstract Syntax [BibTeX] |
1988 | Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), pp. 199-208 | inproceedings | |

BibTeX:
@inproceedings{FPCE:88, author = {Frank Pfenning and Conal Elliot}, title = {Higher-Order Abstract Syntax}, booktitle = {Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI)}, year = {1988}, pages = {199--208} } |
|||||

Pientka, B. & Pfenning, F. | Optimizing Higher-Order Pattern Unification [BibTeX] |
2003 | CADE, pp. 473-487 | inproceedings | |

BibTeX:
@inproceedings{BPFP:03, author = {Brigitte Pientka and Frank Pfenning}, title = {Optimizing Higher-Order Pattern Unification}, booktitle = {CADE}, year = {2003}, pages = {473-487} } |
|||||

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} } |
|||||

Pierro, A.D., Hankin, C. & Wiklicky, H. | On Reversible Combinatory Logic [BibTeX] |
2006 | Mathematical Structures in Computer Science Vol. 16(4), pp. 621-637 |
article | DOI |

BibTeX:
@article{Pie:06, author = {Alessandra Di Pierro and Chris Hankin and Herbert Wiklicky}, title = {On Reversible Combinatory Logic}, journal = {Mathematical Structures in Computer Science}, year = {2006}, volume = {16}, number = {4}, pages = {621--637}, note = {http://dx.doi.org/10.1016/j.entcs.2005.09.018Electronic Edition}, doi = {http://dx.doi.org/10.1017/S0960129506005391} } |
|||||

Pitts, A.M. | Nominal Logic: A First Order Theory of Names and Binding [BibTeX] |
2001 | TACS, pp. 219-242 | inproceedings | URL |

BibTeX:
@inproceedings{AP:01, author = {Andrew M. Pitts}, title = {Nominal Logic: A First Order Theory of Names and Binding}, booktitle = {TACS}, year = {2001}, pages = {219-242}, url = {http://link.springer.de/link/service/series/0558/bibs/2215/22150219.htm} } |
|||||

Pitts, A.M. | Parametric polymorphism and operational equivalence [BibTeX] |
2000 | Mathematical Structures in Computer Science Vol. 10(3), pp. 321-359 |
article | |

BibTeX:
@article{AP:00, author = {Andrew M. Pitts}, title = {Parametric polymorphism and operational equivalence}, journal = {Mathematical Structures in Computer Science}, year = {2000}, volume = {10}, number = {3}, pages = {321--359} } |
|||||

Plotkin, G. | Building in equational theories [BibTeX] |
1972 | Machine Intelligence Vol. 7, pp. 73-90 |
article | URL |

BibTeX:
@article{Plo:72, author = {G. Plotkin}, title = {Building in equational theories}, journal = {Machine Intelligence}, publisher = {Edinburgh University Press}, year = {1972}, volume = {7}, pages = {73--90}, note = {http://www.cs.york.ac.uk/mlg/MI/mi.htmlJournal Webpage}, url = {http://www.cs.york.ac.uk/mlg/MI/mi.html} } |
|||||

Pollack, R. | Closure Under Alpha-Conversion [BibTeX] |
1993 | TYPES, pp. 313-332 | inproceedings | |

BibTeX:
@inproceedings{RP:93, author = {Randy Pollack}, title = {Closure Under Alpha-Conversion}, booktitle = {TYPES}, year = {1993}, pages = {313-332} } |
|||||

Prehofer, C. | Solving Higher-Order Equations: From Logic to Programming [BibTeX] |
1995 | School: Technische Universität München |
phdthesis | |

BibTeX:
@phdthesis{Pre:95, author = {C. Prehofer}, title = {Solving Higher-Order Equations: From Logic to Programming}, school = {Technische Universität München}, year = {1995}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.3626Electronic Edition} } |
|||||

Prehofer, C. | Decidable higher-order unification problems [BibTeX] |
1994 | Lecture Notes in Computer Science Vol. 814, pp. 635-?? |
article | |

BibTeX:
@article{CP:94, author = {C. Prehofer}, title = {Decidable higher-order unification problems}, journal = {Lecture Notes in Computer Science}, year = {1994}, volume = {814}, pages = {635--??} } |
|||||

Pym, D. | Proofs, Search and Computation in General Logic [BibTeX] |
1990 | (CST-69-90)School: Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh |
phdthesis | URL |

BibTeX:
@phdthesis{Pym:90, author = {D. Pym}, title = {Proofs, Search and Computation in General Logic}, school = {Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh}, year = {1990}, number = {CST-69-90}, note = {http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-125/Electronic Edition}, url = {http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-125/} } |
|||||

R. Milner, M. Tofte, R.H. | The Standard Meta Language of New Jersey [BibTeX] |
1974 | other | ||

BibTeX:
@other{SML, author = {R. Milner, M. Tofte, R. Harper}, title = {The Standard Meta Language of New Jersey}, year = {1974}, note = {http://www.smlnj.org/Website} } |
|||||

van Raamsdonk, F. | Higher-Order Rewriting [BibTeX] |
1999 | Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99), pp. 45-59 | inproceedings | |

BibTeX:
@inproceedings{FR:99, author = {Femke van Raamsdonk}, title = {Higher-Order Rewriting}, booktitle = {Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99)}, publisher = {Springer-Verlag LNCS 1631}, year = {1999}, pages = {45--59}, note = {Invited Tutorial} } |
|||||

Ramnath, S. & Zhao, P. | On the isomorphism of expressions [BibTeX] |
2000 | Information and Processing Letters. Vol. 74(3-4), pp. 97-102 |
article | |

BibTeX:
@article{SRPZ:00, author = {Sarnath Ramnath and Peiyi Zhao}, title = {On the isomorphism of expressions}, journal = {Information and Processing Letters.}, publisher = {Elsevier Science B.V. (North Holland)}, year = {2000}, volume = {74}, number = {3-4}, pages = {97--102} } |
|||||

Ramsey, F.P. | The Foundations of Mathematics [BibTeX] |
1925 | Proceedings of the London Mathematical Society, Series 2 Vol. 25(5), pp. 338-384 |
article | |

BibTeX:
@article{Ram:25, author = {F. P. Ramsey}, title = {The Foundations of Mathematics}, journal = {Proceedings of the London Mathematical Society, Series 2}, year = {1925}, volume = {25}, number = {5}, pages = {338--384} } |
|||||

Riecke, J.G. | Statman's 1-Section Theorem [BibTeX] |
1995 | Information and Computation Vol. 116, pp. 275-293 |
article | |

BibTeX:
@article{JR:95, author = {Jon G. Riecke}, title = {Statman's 1-Section Theorem}, journal = {Information and Computation}, year = {1995}, volume = {116}, pages = {275--293} } |
|||||

Rittri, M. | Using types as search keys in function libraries [BibTeX] |
1991 | Journal of Functional Programming Vol. 1(1), pp. 71-89 |
article | URL |

BibTeX:
@article{Rit:91, author = {M. Rittri}, title = {Using types as search keys in function libraries}, journal = {Journal of Functional Programming}, year = {1991}, volume = {1}, number = {1}, pages = {71--89}, note = {http://dx.doi.org/10.1145/99370.99384Electronic Edition}, url = {http://dx.doi.org/10.1145/99370.99384} } |
|||||

Rittri, M. | Retrieving Library Identifiers via Equational Matching of Types [BibTeX] |
1990 | Vol. 44910th International Conference on Automated Deduction, pp. 603-617 |
inproceedings | |

BibTeX:
@inproceedings{Rit:97, author = {M. Rittri}, title = {Retrieving Library Identifiers via Equational Matching of Types}, booktitle = {10th International Conference on Automated Deduction}, publisher = {Springer Verlag}, year = {1990}, volume = {449}, pages = {603-617}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.4344Electronic Edition} } |
|||||

Robinson, J.A. | Mechanizing Higher-Order Logic [BibTeX] |
1969 | Vol. 4Machine Intelligence , pp. 151-170 |
inproceedings | URL |

BibTeX:
@inproceedings{Rob:69, author = {J. A. Robinson}, title = {Mechanizing Higher-Order Logic}, booktitle = {Machine Intelligence }, publisher = {Edinburgh University Press}, year = {1969}, volume = {4}, pages = {151--170}, note = {Journal http://www.cs.york.ac.uk/mlg/MI/mi.htmlJournal Webpage}, url = {http://www.cs.york.ac.uk/mlg/MI/mi.html} } |
|||||

Robinson, J.A. | A Review of Automatic Theorem-Proving [BibTeX] |
1967 | Proceedings of Annual Symposium in Applied Mathematics XIX, pp. 1-18 | inproceedings | |

BibTeX:
@inproceedings{Rob:67, author = {J. A. Robinson}, title = {A Review of Automatic Theorem-Proving}, booktitle = {Proceedings of Annual Symposium in Applied Mathematics XIX}, year = {1967}, pages = {1--18} } |
|||||

Robinson, J.A. | A machine-oriented logic based on the resolution principle [BibTeX] |
1965 | Journal of the ACM Vol. 12(1), pp. 23-41 |
article | DOI |

BibTeX:
@article{Rob:65, author = {J. A. Robinson}, title = {A machine-oriented logic based on the resolution principle}, journal = {Journal of the ACM}, year = {1965}, volume = {12}, number = {1}, pages = {23--41}, note = {http://doi.acm.org/10.1145/321250.321253Electronic Edition}, doi = {http://doi.acm.org/10.1145/321250.321253} } |
|||||

Rollins, E. & Wing, J. | Specifications as Search Keys for Software Libraries [BibTeX] |
1991 | 8th International Conference on Logic Programming, pp. 173-187 | inproceedings | |

BibTeX:
@inproceedings{RW:91, author = {E. Rollins and J. Wing}, title = {Specifications as Search Keys for Software Libraries}, booktitle = {8th International Conference on Logic Programming}, publisher = {MIT press}, year = {1991}, pages = {173--187}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.8746Electronic Edition} } |
|||||

Runciman, C. & Toyn, I. | Retrieving Reusable Software Components by Polymorphic Type [BibTeX] |
1991 | Journal of Functional Programming Vol. 1(2), pp. 191-211 |
article | |

BibTeX:
@article{RT:91, author = {C. Runciman and I. Toyn}, title = {Retrieving Reusable Software Components by Polymorphic Type}, journal = {Journal of Functional Programming}, year = {1991}, volume = {1}, number = {2}, pages = {191--211}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.6545Electronic Edition} } |
|||||

Russell, B. | Mathematical logic as based on the theory of types [BibTeX] |
1908 | American Journal of Mathematics Vol. 30, pp. 222-262 |
article | URL |

BibTeX:
@article{Rus:08, author = {B. Russell}, title = {Mathematical logic as based on the theory of types}, journal = {American Journal of Mathematics}, year = {1908}, volume = {30}, pages = {222--262}, note = {http://www.jstor.org/stable/2369948Electronic Edition}, url = {http://www.jstor.org/stable/2369948} } |
|||||

Russell, B. | The Principles of Mathematics [BibTeX] |
1903 | book | ||

BibTeX:
@book{Rus:03, author = {B. Russell}, title = {The Principles of Mathematics}, publisher = {Cambridge University Press}, year = {1903} } |
|||||

S.P. Lones, P.W. | Haskell: A purely functional programming language [BibTeX] |
1990 | other | ||

BibTeX:
@other{HASKELL, author = {S. P. Lones, P. Walder}, title = {Haskell: A purely functional programming language}, year = {1990}, note = { http://www.haskell.org/Website} } |
|||||

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} } |
|||||

Sazeides, Y. | Instruction-Isomorphism in Program Execution [BibTeX] |
2003 | Journal of Instruction-Level Parallelism Vol. 5 |
article | URL |

BibTeX:
@article{YS:03, author = {Yiannakis Sazeides}, title = {Instruction-Isomorphism in Program Execution}, journal = {Journal of Instruction-Level Parallelism}, year = {2003}, volume = {5}, url = {http://www.jilp.org/vol5/v5paper13.pdf} } |
|||||

Schmidt-Schauß, M. & Schulz, K.U. | Decidability of bounded higher-order unification [BibTeX] |
2005 | Journal of Symbolic Computation Vol. 40(2), pp. 905-954 |
article | |

BibTeX:
@article{MSSKS:05, author = {Manfred Schmidt-Schauß and Klaus U. Schulz}, title = {Decidability of bounded higher-order unification}, journal = {Journal of Symbolic Computation}, year = {2005}, volume = {40}, number = {2}, pages = {905--954} } |
|||||

Schubert, A. | Linear Interpolation for the Higher-Order Matching Problem [BibTeX] |
1997 | TAPSOFT, pp. 441-452 | inproceedings | |

BibTeX:
@inproceedings{AS:97, author = {Aleksy Schubert}, title = {Linear Interpolation for the Higher-Order Matching Problem}, booktitle = {TAPSOFT}, year = {1997}, pages = {441-452} } |
|||||

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} } |
|||||

Sethi, R. | Errata: ``Testing for the Church-Rosser Property'' [BibTeX] |
1975 | Journal of the ACM Vol. 22(3), pp. 424-424 |
article | |

BibTeX:
@article{RS:75, author = {Ravi Sethi}, title = {Errata: ``Testing for the Church-Rosser Property''}, journal = {Journal of the ACM}, year = {1975}, volume = {22}, number = {3}, pages = {424--424}, note = {See teSethi:1974:TCR.} } |
|||||

Severi, P. & de Vries, F. | An Extensional Böhm Model [BibTeX] |
2002 | Vol. 2378Proc. of 13th Int. Conf. on Rewriting Theory and Applications, RTA 2002, Copenhagen, Denmark, 22--24 July 2002, pp. 159-173 |
incollection | |

BibTeX:
@incollection{PSFdV:02, author = {Paula Severi and Fer-Jan de Vries}, title = {An Extensional Böhm Model}, booktitle = {Proc. of 13th Int. Conf. on Rewriting Theory and Applications, RTA 2002, Copenhagen, Denmark, 22--24 July 2002}, publisher = {Springer-Verlag}, year = {2002}, volume = {2378}, pages = {159--173} } |
|||||

Shamir, R. & Tsur, D. | Faster subtree isomorphism [BibTeX] |
1999 | Journal of Algorithms Vol. 33(2), pp. 267-280 |
article | |

BibTeX:
@article{RSDT:99, author = {Ron Shamir and Dekel Tsur}, title = {Faster subtree isomorphism}, journal = {Journal of Algorithms}, publisher = {Academic Press}, year = {1999}, volume = {33}, number = {2}, pages = {267--280} } |
|||||

Shoenfield, J.R. | The Mathematical Work of S. C. Kleene [BibTeX] |
1995 | Bulletin of Symbolic Logic Vol. 1, pp. 9-43 |
article | |

BibTeX:
@article{JS:95, author = {Joseph R. Shoenfield}, title = {The Mathematical Work of S. C. Kleene}, journal = {Bulletin of Symbolic Logic}, year = {1995}, volume = {1}, pages = {9--43} } |
|||||

Snyder, W. & Gallier, J. | Higher Order Unification Revisited: Complete Sets of Transformations [BibTeX] |
1989 | Journal of Symbolic Computation Vol. 8(1 \& 2), pp. 101-140 |
article | DOI |

BibTeX:
@article{SG:89, author = {W. Snyder and J. Gallier}, title = {Higher Order Unification Revisited: Complete Sets of Transformations}, journal = {Journal of Symbolic Computation}, year = {1989}, volume = {8}, number = {1 & 2}, pages = {101--140}, note = {http://dx.doi.org/10.1016/S0747-7171(89)80023-9Electronic Edition.}, doi = {http://dx.doi.org/10.1016/S0747-7171(89)80023-9} } |
|||||

Soloviev, S. | A Complete Axiom System for Isomorphism of Types in Closed Categories [BibTeX] |
1993 | Vol. 698LPAR '93: Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning, pp. 360-371 |
inproceedings | |

BibTeX:
@inproceedings{Sol:93, author = {S. Soloviev}, title = {A Complete Axiom System for Isomorphism of Types in Closed Categories}, booktitle = {LPAR '93: Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning}, publisher = {Springer-Verlag}, year = {1993}, volume = {698}, pages = {360--371}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.1383Electronic Edition} } |
|||||

Soloviev, S. | The category of finite sets and cartesian closed categories [BibTeX] |
1983 | Journal of Soviet Mathematics (Doklady Mathematics) Vol. 22, pp. 1387-1400 |
article | URL |

BibTeX:
@article{Sol:83, author = {S. Soloviev}, title = {The category of finite sets and cartesian closed categories}, journal = {Journal of Soviet Mathematics (Doklady Mathematics)}, year = {1983}, volume = {22}, pages = {1387--1400}, note = {http://www.maik.rssi.ru/cgi-bin/journal.pl?name=danmathJournal Webpage}, url = {http://www.maik.rssi.ru/cgi-bin/journal.pl?name=danmath&page=main} } |
|||||

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} } |
|||||

Steele, G.L. | Building Interpreters by Composing Monads [BibTeX] |
1994 | Principles of Programming Languages | inproceedings | URL |

BibTeX:
@inproceedings{GS:94, author = {Guy L. Steele}, title = {Building Interpreters by Composing Monads}, booktitle = {Principles of Programming Languages}, year = {1994}, url = {http://www-swiss.ai.mit.edu/ftpdir/users/dae/related-papers/steele.ps.Z} } |
|||||

Stirling, C. | Decidability of higher-order matching [BibTeX] |
2008 | unpublished | ||

BibTeX:
@unpublished{Col:06, author = {C. Stirling}, title = {Decidability of higher-order matching}, year = {2008}, note = {http://homepages.inf.ed.ac.uk/cps/lmcs.psElectronic Edition} } |
|||||

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} } |
|||||

Stirling, C. | Higher-Order Matching, Games and Automata [BibTeX] |
2007 | LICS, pp. 326-335 | inproceedings | URL |

BibTeX:
@inproceedings{CS:07a, author = {Colin Stirling}, title = {Higher-Order Matching, Games and Automata}, booktitle = {LICS}, publisher = {IEEE Computer Society}, year = {2007}, pages = {326--335}, url = {http://doi.ieeecomputersociety.org/10.1109/LICS.2007.23} } |
|||||

Stirling, C. | Games, Automata and Matching [BibTeX] |
2007 | Vol. 4603CADE, pp. 1-2 |
inproceedings | URL |

BibTeX:
@inproceedings{CS:07b, author = {Colin Stirling}, title = {Games, Automata and Matching}, booktitle = {CADE}, publisher = {Springer}, year = {2007}, volume = {4603}, pages = {1--2}, url = {http://dx.doi.org/10.1007/978-3-540-73595-3_1} } |
|||||

Stirling, C. | Higher-Order Matching and Games [BibTeX] |
2005 | Vol. 3634Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL Oxford, UK, August 22-25, 2005, Proceedings, pp. 119-134 |
inproceedings | DOI |

BibTeX:
@inproceedings{Col:05, author = {C. Stirling}, title = {Higher-Order Matching and Games}, booktitle = {Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL Oxford, UK, August 22-25, 2005, Proceedings}, publisher = {Springer Verlag}, year = {2005}, volume = {3634}, pages = {119--134}, note = {http://dx.doi.org/10.1007/11538363_10Electronic Edition}, doi = {http://dx.doi.org/10.1007/11538363_10} } |
|||||

Tarau, P. | Declarative Combinatorics: Boolean Functions, Circuit Synthesis and BDDs in Haskell | 2008 | misc | URL | |

Abstract: We describe Haskell implementations of interesting combinatorial generation algorithms with focus on boolean functions and logic circuit representations. First, a complete exact combinational logic circuit synthesizer is described as a combination of catamorphisms and anamorphisms. Using pairing and unpairing functions on natural number representations of truth tables, we derive an encoding for Binary Decision Diagrams (BDDs) with the unique property that its boolean evaluation faithfully mimics its structural conversion to a a natural number through recursive application of a matching pairing function. We then use this result to derive ranking and unranking functions for BDDs and reduced BDDs. Finally, a generalization of the encoding techniques to Multi-Terminal BDDs is provided. The paper is organized as a self-contained literate Haskell program, available at http://logic.csci.unt.edu/tarau/research/2008/fBDD.zip . Keywords: exact combinational logic synthesis, binary decision diagrams, encodings of boolean functions, pairing/unpairing functions, ranking/unranking functions for BDDs and MTBDDs, declarative combinatorics in Haskell |
|||||

BibTeX:
@misc{PT:08, author = {Paul Tarau}, title = {Declarative Combinatorics: Boolean Functions, Circuit Synthesis and BDDs in Haskell}, year = {2008}, note = {Comment: unpublished draft}, url = {http://arxiv.org/abs/0808.0760} } |
|||||

Taylor, P. | Practical Foundations of Mathematics [BibTeX] |
1999 | book | ||

BibTeX:
@book{PT:99, author = {P. Taylor}, title = {Practical Foundations of Mathematics}, publisher = {Cambridge University Press}, year = {1999}, note = {http://www.cs.man.ac.uk/~pt/Practical_Foundations/html/summary.htmlElectronic Edition} } |
|||||

Thatte, S.R. | Coercive Type Isomorphism [BibTeX] |
1991 | Lecture Notes in Computer Science Vol. 523, pp. 29-?? |
article | |

BibTeX:
@article{SaT:91, author = {Satish R. Thatte}, title = {Coercive Type Isomorphism}, journal = {Lecture Notes in Computer Science}, year = {1991}, volume = {523}, pages = {29--??} } |
|||||

Thompson, S. | Refactoring Functional Programs [BibTeX] |
2004 | Advanced Functional Programming, pp. 331-357 | inproceedings | DOI |

BibTeX:
@inproceedings{ST:04, author = {Simon Thompson}, title = {Refactoring Functional Programs}, booktitle = {Advanced Functional Programming}, year = {2004}, pages = {331-357}, doi = {http://dx.doi.org/10.1007/11546382_9} } |
|||||

Thompson, S. | Functional Programming: Executable Specifications and Program Transformation [BibTeX] |
1989 | Proceedings of the 5th International Workshop on Software Specification and Design, pp. 287-290 | inproceedings | |

BibTeX:
@inproceedings{ST:89, author = {S. Thompson}, title = {Functional Programming: Executable Specifications and Program Transformation}, booktitle = {Proceedings of the 5th International Workshop on Software Specification and Design}, publisher = {IEEE Computer Society Press}, year = {1989}, pages = {287--290} } |
|||||

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} } |
|||||

Urban, C., Pitts, A.M. & Gabbay, M. | Nominal unification [BibTeX] |
2004 | Theoretical Computer Science Vol. 323(1-3), pp. 473-497 |
article | DOI |

BibTeX:
@article{UPG:04, author = {Christian Urban and Andrew M. Pitts and Murdoch Gabbay}, title = {Nominal unification}, journal = {Theoretical Computer Science}, year = {2004}, volume = {323}, number = {1-3}, pages = {473-497}, doi = {http://dx.doi.org/10.1016/j.tcs.2004.06.016} } |
|||||

Visser, E. | A Survey of Rewriting Strategies in Program Transformation Systems [BibTeX] |
2002 | misc | URL | |

BibTeX:
@misc{EV:02, author = {Eelco Visser}, title = {A Survey of Rewriting Strategies in Program Transformation Systems}, year = {2002}, url = {http://www.library.uu.nl/digiarchief/dip/dispute/2002-0308-093116/2001-31.pdf} } |
|||||

Wadler, P. | Monads for functional programming [BibTeX] |
1994 | Vol. 118Program Design Calculi |
incollection | |

BibTeX:
@incollection{PW:94, author = {Philip Wadler}, title = {Monads for functional programming}, booktitle = {Program Design Calculi}, publisher = {Springer Verlag}, year = {1994}, volume = {118}, note = {Proceedings of the International Summer School at Marktoberdorf directed by F. L. Bauer, M. Broy, E. W. Dijkstra, D. Gries, and C. A. R. Hoare} } |
|||||

Wadler, P. | A taste of linear logic [BibTeX] |
1993 | Vol. 711Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, MFCS'93 (Gdańsk, Poland, August 30 - September 3, 1993), pp. 185-210 |
incollection | URL |

BibTeX:
@incollection{PW:93, author = {Philip Wadler}, title = {A taste of linear logic}, booktitle = {Proceedings of the 18th International Symposium on Mathematical Foundations of Computer Science, MFCS'93 (Gdańsk, Poland, August 30 - September 3, 1993)}, publisher = {Springer-Verlag}, year = {1993}, volume = {711}, pages = {185--210}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=711&spage=185} } |
|||||

Wadler, P. | Theorems for Free [BibTeX] |
1989 | 4th International Conference on Functional Programming Languages and Computer Architecture'89., pp. 347-359 | inproceedings | |

BibTeX:
@inproceedings{Wad:89, author = {P. Wadler}, title = {Theorems for Free}, booktitle = {4th International Conference on Functional Programming Languages and Computer Architecture'89.}, publisher = {ACM Press}, year = {1989}, pages = {347--359}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875Electronic Edition} } |
|||||

Wadler, P. | Views: A Way for Pattern Matching to Cohabit with Data Abstraction [BibTeX] |
1987 | Proceedings, 14th Symposium on Principles of Programming Languages, pp. 307-312 | incollection | |

BibTeX:
@incollection{PW:87, author = {Philip Wadler}, title = {Views: A Way for Pattern Matching to Cohabit with Data Abstraction}, booktitle = {Proceedings, 14th Symposium on Principles of Programming Languages}, publisher = {Association for Computing Machinery}, year = {1987}, pages = {307--312} } |
|||||

Wand, M. | Finding the Source of Type Errors [BibTeX] |
1986 | Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, pp. 38-43 | inproceedings | DOI |

BibTeX:
@inproceedings{Wan:86, author = {M. Wand}, title = {Finding the Source of Type Errors}, booktitle = {Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages}, publisher = {ACM Press}, year = {1986}, pages = {38--43}, note = {http://doi.acm.org/10.1145/512644.512648Electronic Edition}, doi = {http://doi.acm.org/10.1145/512644.512648} } |
|||||

Whitehead, A.N. & Russell, B. | Principia Mathematica [BibTeX] |
1925--1927 | book | ||

BibTeX:
@book{WR:25, author = {A. N. Whitehead and B. Russell}, title = {Principia Mathematica}, publisher = {Cambridge University Press}, year = {1925--1927}, edition = {Second}, note = {Three volumes.} } |
|||||

Whitehead, A.N. & Russell, B. | Principia Mathematica [BibTeX] |
1910--1913 | book | ||

BibTeX:
@book{WR:10, author = {A. N. Whitehead and B. Russell}, title = {Principia Mathematica}, publisher = {Cambridge University Press}, year = {1910--1913}, edition = {First}, note = {Three volumes.} } |
|||||

Wierzbicki, T. | Complexity of the higher order matching [BibTeX] |
1999 | CADE, pp. 82-96 | inproceedings | URL |

BibTeX:
@inproceedings{TW:99, author = {Tomasz Wierzbicki}, title = {Complexity of the higher order matching}, booktitle = {CADE}, year = {1999}, pages = {82-96}, url = {http://link.springer.de/link/service/series/0558/bibs/1632/16320082.htm} } |
|||||

Wilkie, A.J. | On Exponentiation - A Solution to Tarski's High School Algebra Problem [BibTeX] |
2000 | Quaderni di Matematica Vol. 6, pp. 107-129 |
article | |

BibTeX:
@article{Wil:81, author = {A. J. Wilkie}, title = {On Exponentiation - A Solution to Tarski's High School Algebra Problem}, journal = {Quaderni di Matematica}, year = {2000}, volume = {6}, pages = {107--129}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.15.9695Electronic Edition} } |
|||||

Xi, H. & Pfenning, F. | Dependent Types in Practical Programming [BibTeX] |
1999 | In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 214-227 | inproceedings | |

BibTeX:
@inproceedings{XP:99, author = {H. Xi and F. Pfenning}, title = {Dependent Types in Practical Programming}, booktitle = {In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages}, publisher = {ACM Press}, year = {1999}, pages = {214--227}, note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.548Electronic Edition} } |
|||||

Yamada, T., Avenhaus, Jü., Loria-Sáenz, C. & Middeldorp, A. | Logicality of conditional rewrite systems [BibTeX] |
2000 | Theoretical Computer Science Vol. 236(1-2), pp. 209-232 |
article | URL |

BibTeX:
@article{TYJACLAM:00, author = {Toshiyuki Yamada and Jürgen Avenhaus and Carlos Loria-Sáenz and Aart Middeldorp}, title = {Logicality of conditional rewrite systems}, journal = {Theoretical Computer Science}, year = {2000}, volume = {236}, number = {1--2}, pages = {209--232}, url = {http://www.elsevier.nl/gej-ng/10/41/16/168/21/27/abstract.html} } |
|||||

Yokoyama, Hu & Takeichi | Deterministic Second-Order Patterns [BibTeX] |
2004 | Information Processing Letters Vol. 89(6), pp. 309 -314 |
article | DOI |

BibTeX:
@article{YHT:04, author = {Yokoyama and Hu and Takeichi}, title = {Deterministic Second-Order Patterns}, journal = {Information Processing Letters}, year = {2004}, volume = {89}, number = {6}, pages = {309 -314}, note = {http://dx.doi.org/10.1016/j.ipl.2003.12.008Electronic Edition}, doi = {http://dx.doi.org/10.1016/j.ipl.2003.12.008} } |
|||||

Yokoyama, T., Hu, Z. & Takeichi, M. | Deterministic Higher-Order Patterns for Program Transformation [BibTeX] |
2003 | LOPSTR, pp. 128-142 | inproceedings | URL |

BibTeX:
@inproceedings{TYZHMT:03, author = {Tetsuo Yokoyama and Zhenjiang Hu and Masato Takeichi}, title = {Deterministic Higher-Order Patterns for Program Transformation}, booktitle = {LOPSTR}, year = {2003}, pages = {128-142}, url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3018&spage=128} } |
|||||

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} } |
|||||

Zermelo, E. | A new proof of the possibility of a well ordering [BibTeX] |
1908 | English translation in From Frege to Gödel, a Source Book in Mathematical Logic (J. van Heijenoort, Editor), Harvard |
misc | |

BibTeX:
@misc{Zer:08, author = {E. Zermelo}, title = {A new proof of the possibility of a well ordering}, year = {1908} } |
|||||

Zibin, Gil & Considine | Efficient Algorithms for Isomorphisms of Simple Types [BibTeX] |
2003 | 30th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 160 - 171 | inproceedings | DOI |

BibTeX:
@inproceedings{ZGC:03, author = {Zibin and Gil and Considine}, title = {Efficient Algorithms for Isomorphisms of Simple Types}, booktitle = {30th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages}, publisher = {ACM Press}, year = {2003}, pages = {160 - 171}, note = {http://dx.doi.org/10.1017/S0960129505004913Electronic Edition}, doi = {http://dx.doi.org/10.1017/S0960129505004913} } |
|||||

Zuliani, P. | Logical reversibility [BibTeX] |
2001 | IBM-Journal of Research and Development Vol. 45(6), pp. 807-818 |
article | URL |

BibTeX:
@article{Zul:01, author = {P. Zuliani}, title = {Logical reversibility}, journal = {IBM-Journal of Research and Development}, year = {2001}, volume = {45}, number = {6}, pages = {807--818}, note = {http://www.research.ibm.com/journal/rd/456/zuliani.htmlElectronic Edition}, url = {http://www.research.ibm.com/journal/rd/456/zuliani.html} } |
|||||

The Coq Proof Assistant [BibTeX] |
1992 | other | URL | ||

BibTeX:
@other{Coq,, title = {The Coq Proof Assistant}, year = {1992}, note = { http://coq.inria.fr/Website}, url = {http://coq.inria.fr/} } |
|||||

PVS Specification and Verification System [BibTeX] |
1992 | other | URL | ||

BibTeX:
@other{PVS,, title = {PVS Specification and Verification System}, year = {1992}, note = { http://pvs.csl.sri.com/Website}, url = {http://pvs.csl.sri.com/} } |

Created by JabRef on 10/12/2008.