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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Created by JabRef on 10/12/2008.