Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings
This book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '98, held in Canberra, Australia, in September/October 1998. The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submiss...
Tallennettuna:
| Yhteisötekijä: | |
|---|---|
| Muut tekijät: | , |
| Aineistotyyppi: | Livre numérique |
| Kieli: | Anglais |
| Julkaistu: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Sarja: | Lecture notes in computer science
1479 |
| Aiheet: | |
| Linkit: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Huomautus: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Theorem proving in higher order logics, 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998, proceedings, Jim Grundy, Malcolm Newey, eds, 1998, Berlin, Springer, 1 vol. (VIII-496 p.), Lecture notes in computer science, 3-540-64987-5 • Theorem Proving in Higher Order Logics, Texte imprimé, 9783662212592 |
Sisällysluettelo:
- Verified lexical analysis
- Extending window inference
- Program abstraction in a higher-order logic framework
- The village telephone system: A case study in formal software engineering
- Generating embeddings from denotational descriptions
- An interface between CLAM and HOL
- Classical propositional decidability via Nuprl proof extraction
- A comparison of PVS and Isabelle/HOL
- Adding external decision procedures to HOL90 securely
- Formalizing basic first order model theory
- Formalizing Dijkstra
- Mechanical verification of total correctness through diversion verification conditions
- A type annotation scheme for Nuprl
- Verifying a garbage collection algorithm
- Hot: A concurrent automated theorem prover based on higher-order tableaux
- Free variables and subexpressions in higher-order meta logic
- An LPO-based termination ordering for higher-order terms without ?-abstraction
- Proving isomorphism of first-order logic proof systems in HOL
- Exploiting parallelism in interactive theorem provers
- I/O automata and beyond: Temporal logic and abstraction in Isabelle
- Object-oriented verification based on record subtyping in Higher-Order Logic
- On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system
- Co-inductive axiomatization of a synchronous language
- Formal specification and theorem proving breakthroughs in geometric modeling
- A tool for data refinement
- Mechanizing relevant logics with HOL
- Case studies in meta-level theorem proving
- Formalization of graph search algorithms and its applications.