Types for proofs and programs : International Workshop TYPES 96 Aussois, France, December 15 19, 1996 : selected papers
This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996. The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 p...
Enregistré dans:
| Collectivité auteur: | |
|---|---|
| Autres auteurs: | , |
| Format: | Livre numérique |
| Langue: | Anglais |
| Publié: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Collection: | Lecture notes in computer science
1512 |
| Sujets: | |
| Accès en ligne: | Acce s sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Types for proofs and programs, International Workshop TYPES '96, Aussois, France, December 1996, selected papers, Eduardo Giménez, Christine Paulin-Mohring (eds.), 1998, Berlin, Springer, 1 vol. (VIII-372 p.), Lecture notes in computer science, 3-540-65137-3 • Types for Proofs and Programs, Texte imprimé, 9783662200575 |
| LEADER | 04128nam a22004457a 4500 | ||
|---|---|---|---|
| 001 | 944978 | ||
| 008 | 110927q2000 xxe ||| |||| 00| 0 eng d | ||
| 009 | PPN155209833 | ||
| 020 | |a 9783540495628 (PDF) | ||
| 041 | 0 | |a eng | |
| 082 | |a 004.015113 | ||
| 082 | |a 004 | ||
| 111 | 2 | |a TYPES |d (1996 |c :Aussois, Savoie). | |
| 245 | 1 | 0 | |a Types for proofs and programs : |b International Workshop TYPES 96 Aussois, France, December 15 19, 1996 : selected papers |c [edited by] Eduardo Giménez, Christine Paulin-Mohring. |
| 260 | |a Berlin [etc.] : |b Springer. | ||
| 260 | |a Cham : |b Springer Nature, |c [20..]. | ||
| 490 | 0 | |a Lecture notes in computer science |v 1512 |x 1611-3349 | |
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 500 | |a Archives Springer e-books (Licence nationale) | ||
| 505 | 0 | |a Coercion synthesis in computer implementations of type-theoretic frameworks -- Verification of the interface of a small proof system in coq -- An implementation of the Heine-Borel covering theorem in type theory -- Detecting and removing dead-code using rank 2 intersection -- A type-free formalization of mathematics where proofs are objects -- Higman's lemma in type theory -- A proof of weak termination of typed ??-calculi -- Proof style -- Some algorithmic and proof-theoretical aspects of coercive subtyping -- Semantical BNF -- The internal type theory of a Heyting pretopos -- Inverting inductively defined relations in LEGO -- A generic normalisation proof for pure type systems -- Proving a real time algorithm for ATM in Coq -- Dependent types with explicit substitutions: A meta-theoretical development -- Type inference verified: Algorithm W in Isabelle/HOL -- Continuous lattices in formal topology -- Abstract insertion sort in an extension of type theory with record types and subtyping. | |
| 506 | |a Accès en ligne pour les établissements français bénéficiaires des licences nationales | ||
| 506 | |a Accès soumis à abonnement pour tout autre établissement | ||
| 506 | |a Conditions particulières de réutilisation pour les bénéficiaires des licences nationales. https://www.licencesnationales.fr/springer-nature-ebooks-contrat-licence-ln-2017 | ||
| 520 | |a This book constitutes the thoroughly revised post-workshop proceedings of the first annual workshop held under the auspices of the ESPRIT Working Group 21900 TYPES in Aussois, France in December 1996. The 18 revised full papers presented in the book were carefully reviewed and selected from the 30 papers accepted for presentation at the workshop. All current aspects of type theory and type systems and their applications to program verification and theorem proving are addressed; the proof systems and theorem provers dealt with include Coq, LEGO, and Isabelle/HOL. | ||
| 650 | |a Informatique | ||
| 650 | |a Langages de programmation | ||
| 650 | |a Intelligence artificielle | ||
| 650 | |a Théorie des types | ||
| 650 | |a Logique symbolique et mathématique | ||
| 650 | |a Logique informatique | ||
| 650 | |a Actes de congrès | ||
| 700 | 1 | |a Giménez, Eduardo, |d 1967- |4 pbd | |
| 700 | 1 | |a Paulin-Mohring, Christine, |d 1962-...., |c informaticienne. |4 pbd | |
| 776 | 0 | |0 045372608 |t Types for proofs and programs |o International Workshop TYPES '96, Aussois, France, December 1996 |o selected papers |f Eduardo Giménez, Christine Paulin-Mohring (eds.) |d 1998 |c Berlin |n Springer |p 1 vol. (VIII-372 p.) |s Lecture notes in computer science |z 3-540-65137-3 | |
| 776 | 0 | |t Types for Proofs and Programs |b Texte imprimé |z 9783662200575 | |
| 856 | 4 | |q PDF |u https://doi.org/10.1007/BFb0097782 |z Acce s sur la plateforme de l'éditeur | |
| 856 | 4 | |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-K258GVHF-5 |z Accès sur la plateforme Istex | |
| 856 | 4 | |5 452349901:747892210 |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/BFb0097782 |z Accès Université d'Orléans | |
| 856 | 4 | |5 180339901:75090531X |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/BFb0097782 |z Accès INSA CVL | |
| 997 | |0 944978 |1 Livre numérique |a Ressource numérique |b INSA |b ENSA |c 0/Bibliothèque numérique/ |c 1/Bibliothèque numérique/Autre ressource numérique/ | ||