![Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers /](/search/themes/bootstrap3/images/libros.png)
Types for Proofs and Programs [electronic resource] : 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 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.
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Texto biblioteca |
| Language: | eng |
| Published: |
Berlin, Heidelberg : Springer Berlin Heidelberg,
1998
|
| Subjects: | Computer science., Software engineering., Programming languages (Electronic computers)., Computer logic., Mathematical logic., Artificial intelligence., Computer Science., Software Engineering/Programming and Operating Systems., Logics and Meanings of Programs., Mathematical Logic and Formal Languages., Programming Languages, Compilers, Interpreters., Artificial Intelligence (incl. Robotics)., |
| Online Access: | http://dx.doi.org/10.1007/BFb0097782 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| id |
KOHA-OAI-TEST:200142 |
|---|---|
| record_format |
koha |
| spelling |
KOHA-OAI-TEST:2001422018-07-30T23:26:48ZTypes for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / Giménez, Eduardo. editor. Paulin-Mohring, Christine. editor. SpringerLink (Online service) textBerlin, Heidelberg : Springer Berlin Heidelberg,1998.engThis 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.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.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.Computer science.Software engineering.Programming languages (Electronic computers).Computer logic.Mathematical logic.Artificial intelligence.Computer Science.Software Engineering/Programming and Operating Systems.Logics and Meanings of Programs.Mathematical Logic and Formal Languages.Programming Languages, Compilers, Interpreters.Artificial Intelligence (incl. Robotics).Springer eBookshttp://dx.doi.org/10.1007/BFb0097782URN:ISBN:9783540495628 |
| institution |
COLPOS |
| collection |
Koha |
| country |
México |
| countrycode |
MX |
| component |
Bibliográfico |
| access |
En linea En linea |
| databasecode |
cat-colpos |
| tag |
biblioteca |
| region |
America del Norte |
| libraryname |
Departamento de documentación y biblioteca de COLPOS |
| language |
eng |
| topic |
Computer science. Software engineering. Programming languages (Electronic computers). Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Software Engineering/Programming and Operating Systems. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Programming Languages, Compilers, Interpreters. Artificial Intelligence (incl. Robotics). Computer science. Software engineering. Programming languages (Electronic computers). Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Software Engineering/Programming and Operating Systems. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Programming Languages, Compilers, Interpreters. Artificial Intelligence (incl. Robotics). |
| spellingShingle |
Computer science. Software engineering. Programming languages (Electronic computers). Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Software Engineering/Programming and Operating Systems. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Programming Languages, Compilers, Interpreters. Artificial Intelligence (incl. Robotics). Computer science. Software engineering. Programming languages (Electronic computers). Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Software Engineering/Programming and Operating Systems. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Programming Languages, Compilers, Interpreters. Artificial Intelligence (incl. Robotics). Giménez, Eduardo. editor. Paulin-Mohring, Christine. editor. SpringerLink (Online service) Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| description |
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. |
| format |
Texto |
| topic_facet |
Computer science. Software engineering. Programming languages (Electronic computers). Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Software Engineering/Programming and Operating Systems. Logics and Meanings of Programs. Mathematical Logic and Formal Languages. Programming Languages, Compilers, Interpreters. Artificial Intelligence (incl. Robotics). |
| author |
Giménez, Eduardo. editor. Paulin-Mohring, Christine. editor. SpringerLink (Online service) |
| author_facet |
Giménez, Eduardo. editor. Paulin-Mohring, Christine. editor. SpringerLink (Online service) |
| author_sort |
Giménez, Eduardo. editor. |
| title |
Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| title_short |
Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| title_full |
Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| title_fullStr |
Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| title_full_unstemmed |
Types for Proofs and Programs [electronic resource] : International Workshop TYPES’96 Aussois, France, December 15–19, 1996 Selected Papers / |
| title_sort |
types for proofs and programs [electronic resource] : international workshop types’96 aussois, france, december 15–19, 1996 selected papers / |
| publisher |
Berlin, Heidelberg : Springer Berlin Heidelberg, |
| publishDate |
1998 |
| url |
http://dx.doi.org/10.1007/BFb0097782 |
| work_keys_str_mv |
AT gimenezeduardoeditor typesforproofsandprogramselectronicresourceinternationalworkshoptypes96aussoisfrancedecember15191996selectedpapers AT paulinmohringchristineeditor typesforproofsandprogramselectronicresourceinternationalworkshoptypes96aussoisfrancedecember15191996selectedpapers AT springerlinkonlineservice typesforproofsandprogramselectronicresourceinternationalworkshoptypes96aussoisfrancedecember15191996selectedpapers |
| _version_ |
1756267387402846208 |