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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Created by JabRef on 10/12/2008.