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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Created by JabRef on 10/12/2008.