| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996466143903316 |
|
|
Titolo |
Higher Order Logic Theorem Proving and Its Applications [[electronic resource] ] : 7th International Workshop, Valletta, Malta, September 19-22, 1994. Proceedings / / edited by Thomas F. Melham, Juanito Camilleri |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1994 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 1994.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XI, 477 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 0302-9743 ; ; 859 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Computers |
Mathematical logic |
Artificial intelligence |
Theory of Computation |
Mathematical Logic and Foundations |
Mathematical Logic and Formal Languages |
Artificial Intelligence |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di contenuto |
|
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. |
|
|
|
|
|
|
Sommario/riassunto |
|
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. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910555236003321 |
|
|
Autore |
Sergey Ilya |
|
|
Titolo |
Programming Languages and Systems : 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings / / edited by Ilya Sergey |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Cham, : Springer Nature, 2022 |
|
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2022 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
|
|
Edizione |
[1st ed. 2022.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (xiv, 604 pages) : illustrations |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Computer Science, , 1611-3349 ; ; 13240 |
|
|
|
|
|
|
Altri autori (Persone) |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Compilers (Computer programs) |
Computer science |
Microprogramming |
Computer networks |
Computer programming |
Compilers and Interpreters |
Theory of Computation |
Control Structures and Microprogramming |
Computer Communication Networks |
Programming Techniques |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
Includes author index. |
|
|
|
|
|
|
|
|
Nota di contenuto |
|
Categorical Foundation of Gradient-Based Learning -- Compiling Universal Probabilistic Programming Languages with Efficient Parallel Sequential Monte Carlo Inference -- Foundations for Entailment Checking in Quantitative Separation Logic -- Extracting total Amb programs from proofs -- Why3-do: The Way of Harmonious Distributed System Proofs -- Relaxed virtual memory in Armv8-A -- Verified Security for the Morello Capability-enhanced Prototype Arm |
|
|
|
|
|
|
|
|
|
|
|
Architecture -- The Trusted Computing Base of the CompCert Verified Compiler -- View-Based Owicki-Gries Reasoning for Persistent x86-TSO -- Abstraction for Crash-Resilient Objects -- Static Race Detection for Periodic Programs -- Probabilistic Total Store Ordering -- Linearity and Uniqueness: An Entente Cordiale -- A Framework for Substructural Type Systems -- A Dependent Dependency Calculus -- Polarized Subtyping -- Structured Handling of Scoped Effects -- Region-based Resource Management and Lexical Exception Handlers in Continuation-Passing Style -- A Predicate Transformer for Choreographies -- Comparing the expressiveness of the -calculus and CCS -- Concurrent NetKAT. |
|
|
|
|
|
|
Sommario/riassunto |
|
This open access book constitutes the proceedings of the 31st European Symposium on Programming, ESOP 2022, which was held during April 5-7, 2022, in Munich, Germany, as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022. The 21 regular papers presented in this volume were carefully reviewed and selected from 64 submissions. They deal with fundamental issues in the specification, design, analysis, and implementation of programming languages and systems. |
|
|
|
|
|
|
|
| |