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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Created by JabRef on 10/12/2008.