Search dblp for Publications

export results for "toc:db/conf/types/types96.bht:"

 download as .bib file

@proceedings{DBLP:conf/types/1996,
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  publisher    = {Springer},
  year         = {1998},
  url          = {https://doi.org/10.1007/BFb0097782},
  doi          = {10.1007/BFB0097782},
  isbn         = {3-540-65137-3},
  timestamp    = {Tue, 14 May 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/1996.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Bailey96,
  author       = {Anthony Bailey},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Coercion Synthesis in Computer Implementations of Type-Theoretic Frameworks},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {9--27},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097784},
  doi          = {10.1007/BFB0097784},
  timestamp    = {Tue, 14 May 2019 10:00:42 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Bailey96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Barras96,
  author       = {Bruno Barras},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Verification of the Interface of a Small Proof System in Coq},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {28--45},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097785},
  doi          = {10.1007/BFB0097785},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Barras96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Cederquist96,
  author       = {Jan Cederquist},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {An Implementation of the Heine-Borel Covering Theorem in Type Theory},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {46--65},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097786},
  doi          = {10.1007/BFB0097786},
  timestamp    = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Cederquist96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Dowek96,
  author       = {Gilles Dowek},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {A Type-Free Formalization of Mathematics where Proofs are Objects},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {88--111},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097788},
  doi          = {10.1007/BFB0097788},
  timestamp    = {Fri, 30 Nov 2018 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/types/Dowek96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Fridlender96,
  author       = {Daniel Fridlender},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Highman's Lemma in theory},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {112--133},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097789},
  doi          = {10.1007/BFB0097789},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Fridlender96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/GimenezP96,
  author       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Introduction},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {1--8},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097783},
  doi          = {10.1007/BFB0097783},
  timestamp    = {Tue, 23 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/GimenezP96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Goubault-Larrecq96,
  author       = {Jean Goubault{-}Larrecq},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {A Proof of Weak Termination of Typed lambda-sigma-Calculi},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {134--153},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097790},
  doi          = {10.1007/BFB0097790},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Goubault-Larrecq96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Harrison96,
  author       = {John Harrison},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Proof Style},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {154--172},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097791},
  doi          = {10.1007/BFB0097791},
  timestamp    = {Thu, 05 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Harrison96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/JonesLS96,
  author       = {Alex P. Jones and
                  Zhaohui Luo and
                  Sergei Soloviev},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Some Algorithmic and Proof-Theoretical Aspects of Coercive Subtyping},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {173--195},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097792},
  doi          = {10.1007/BFB0097792},
  timestamp    = {Tue, 02 Jan 2018 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/types/JonesLS96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Maenpaa96,
  author       = {Petri M{\"{a}}enp{\"{a}}{\"{a}}},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Semantical {BNF}},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {196--215},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097793},
  doi          = {10.1007/BFB0097793},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Maenpaa96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Maietti96,
  author       = {Maria Emilia Maietti},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {The Internal Type Theory of a Heyting Pretopos},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {216--235},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097794},
  doi          = {10.1007/BFB0097794},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Maietti96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/McBride96,
  author       = {Conor McBride},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Inverting Inductively Defined Relations in {LEGO}},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {236--253},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097795},
  doi          = {10.1007/BFB0097795},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/McBride96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/MelliesW96,
  author       = {Paul{-}Andr{\'{e}} Melli{\`{e}}s and
                  Benjamin Werner},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {A Generic Normalisation Proof for Pure Type Systems},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {254--276},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097796},
  doi          = {10.1007/BFB0097796},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/MelliesW96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Monin96,
  author       = {Jean{-}Fran{\c{c}}ois Monin},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Proving a Real Time Algorithm for {ATM} in Coq},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {277--293},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097797},
  doi          = {10.1007/BFB0097797},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Monin96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Munoz96,
  author       = {C{\'{e}}sar A. Mu{\~{n}}oz},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Dependent Types with Explicit Substitutiuons: {A} Meta-theoretical
                  development},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {294--316},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097798},
  doi          = {10.1007/BFB0097798},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Munoz96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/NaraschewskiN96,
  author       = {Wolfgang Naraschewski and
                  Tobias Nipkow},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Type Inference Verified: Algorithm {W} in Isabelle/HOL},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {317--332},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097799},
  doi          = {10.1007/BFB0097799},
  timestamp    = {Sat, 30 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/NaraschewskiN96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Negri96,
  author       = {Sara Negri},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Continous Lattices in Formal Topology},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {333--353},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097800},
  doi          = {10.1007/BFB0097800},
  timestamp    = {Sun, 21 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Negri96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Prost96,
  author       = {Ferruccio Damiani and
                  Fr{\'{e}}d{\'{e}}ric Prost},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Detecting and Removing Dead-Code using Rank 2 Intersection},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {66--87},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097787},
  doi          = {10.1007/BFB0097787},
  timestamp    = {Fri, 30 Nov 2018 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/types/Prost96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/types/Tasistro96,
  author       = {Alvaro Tasistro},
  editor       = {Eduardo Gim{\'{e}}nez and
                  Christine Paulin{-}Mohring},
  title        = {Abstract Insertion Sort in an Extension of Type Theory with Record
                  Types and Subtyping},
  booktitle    = {Types for Proofs and Programs, International Workshop TYPES'96, Aussois,
                  France, December 15-19, 1996, Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {1512},
  pages        = {354--372},
  publisher    = {Springer},
  year         = {1996},
  url          = {https://doi.org/10.1007/BFb0097801},
  doi          = {10.1007/BFB0097801},
  timestamp    = {Sat, 30 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/types/Tasistro96.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.