Higher order logic theorem proving and its application : 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings
This volume presents the proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications held in Valetta, Malta in September 1994. Besides 3 invited papers, the proceedings contains 27 refereed papers selected from 42 submissions. In total the book presents m...
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
859 |
| Sujets: | |
| Accès en ligne: | Accè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: | • Higher order logic theorem proving and its application, 7th international workshop, Valletta, Malta, September 19-22, 1994, proceedings, Thomas F. Melham, Juanito Camilleri, (eds.), Berlin, Springer-Verlag, 1994, 1 vol. (IX-470 p.), Lecture notes in computer science, 3-540-58450-1 • Higher Order Logic Theorem Proving and Its Applications, Texte imprimé, 9783662214749 |
Table des matières:
- LCF examples in HOL
- A graphical tool for proving UNITY progress
- Reasoning about a class of linear systems of equations in HOL
- Towards a HOL theory of memory
- Providing tractable security analyses in HOL
- Highlighting the lambda-free fragment of Automath
- First-order automation for higher-order-logic theorem proving
- Symbolic animation as a proof tool
- Datatypes in L2
- A formal theory of undirected graphs in higher-order logc
- Mechanical verification of distributed algorithms in higher-order logic
- Tracking design changes with formal verification
- Weak systems of set theory related to HOL
- Interval-semantic component models and the efficient verification of transaction-level circuit behavior
- An interpretation of Noden in HOL
- Reasoning about real circuits
- Binary decision diagrams as a HOL derived rule
- Trustworthy tools for trustworthy programs: A verified verification condition generator
- S: A machine readable specification notation based on higher order logic.-An engineering approach to formal digital system design
- Generating designs using an Algorithmic Register Transfer Language with formal semantics
- A HOL formalisation of the Temporal Logic of Actions
- Studying the ML module system in HOL
- Towards a mechanically supported and compositional calculus to design distributed algorithms
- Simplifying deep embedding: A formalised code generator
- Automating verification by functional abstraction at the system level
- A parameterized proof manager
- Implementational issues for verifying RISC-pipeline conflicts in HOL
- Specifying instruction-set architectures in HOL: A primer
- Representing higher-order logic proofs in HOL.