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...

Full description

Saved in:
Bibliographic Details
Corporate Author: International workshop on Higher Order Logic Theorem Proving and its Applications :La Valette
Other Authors: Camilleri, Juanito (Publishing director), Melham, Thomas F., 1960- (Publishing director)
Format: Livre numérique
Language:Anglais
Published: Berlin [etc.] : Springer [20..].
Cham : Springer Nature
Series:Lecture notes in computer science 859
Subjects:
Online Access: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
LEADER 04899nam a22004217a 4500
001 944432
008 110927q2000 xxe ||| |||| 00| 0 eng d
009 PPN155188003
020 |a 9783540488033 (PDF) 
041 0 |a eng 
082 |a 004 
082 |a 004.015113 
111 2 |a International workshop on Higher Order Logic Theorem Proving and its Applications  |n (07  |d  :1994  |c  :La Valette). 
245 1 0 |a Higher order logic theorem proving and its application :  |b 7th international workshop, Valletta, Malta, September 19-22, 1994 : proceedings   |c [edited by] Thomas F. Melham, Juanito Camilleri. 
260 |a Berlin [etc.] :  |b Springer. 
260 |a Cham :  |b Springer Nature,  |c [20..]. 
490 0 |a Lecture notes in computer science  |v 859  |x 1611-3349 
500 |a Archives Springer e-books (Licence nationale) 
500 |a Archives Springer e-books (Licence nationale) 
505 0 |a 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. 
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 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 many new results by leading researchers working on the design and applications of theorem provers for higher order logic. In particular, this book gives a thorough state-of-the-art report on applications of the HOL system, one of the most widely used theorem provers for higher order logic. 
650 |a Informatique 
650 |a Intelligence artificielle 
650 |a Logique symbolique et mathématique 
650 |a Théorèmes  |x Démonstration automatique 
650 |a Actes de congrès 
700 1 |a Camilleri, Juanito.  |4 pbd 
700 1 |a Melham, Thomas F.,  |d 1960-  |4 pbd 
776 0 |0 021376131  |t Higher order logic theorem proving and its application  |o 7th international workshop, Valletta, Malta, September 19-22, 1994  |o proceedings  |f Thomas F. Melham, Juanito Camilleri, (eds.)  |c Berlin  |n Springer-Verlag  |d 1994  |p 1 vol. (IX-470 p.)  |s Lecture notes in computer science  |z 3-540-58450-1 
776 0 |t Higher Order Logic Theorem Proving and Its Applications  |b Texte imprimé  |z 9783662214749 
856 4 |q PDF  |u https://doi.org/10.1007/3-540-58450-1  |z Accès sur la plateforme de l'éditeur 
856 4 |u https://revue-sommaire.istex.fr/ark:/67375/8Q1-7JCBDNCH-7  |z Accès sur la plateforme Istex 
856 4 |5 452349901:747919682  |u https://ezproxy.univ-orleans.fr/login?url=https://doi.org/10.1007/3-540-58450-1  |z Accès Université d'Orléans 
856 4 |5 180339901:750932201  |u https://ezproxy.insa-cvl.fr/login?qurl=https://doi.org/10.1007/3-540-58450-1  |z Accès INSA CVL 
997 |0 944432  |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/