Cantitate/Preț
Produs
Total produse
Vezi coșul
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings de Sandrine Blazy

Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013, Proceedings: Lecture Notes in Computer Science, cartea 7998

Editat de Sandrine Blazy, Christine Paulin-Mohring, David Pichardie
en Limba Engleză Paperback – 19 iul 2013
This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013. The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.
Citește tot Restrânge

Din seria Lecture Notes in Computer Science

Preț: 33606 lei

Preț vechi: 42008 lei
-20% Nou

Puncte Express: 504
Preț estimativ în valută:
6434€ • 6687$ • 5334£

Carte tipărită la comandă

Livrare economică 05-19 februarie 25

 Adaugă în coș

Wish list
Gift list
Am citit!
Adaugă în listă
Preluare comenzi: 021 569.72.76

Specificații

ISBN-13: 9783642396335
ISBN-10: 364239633X
Pagini: 512
Ilustrații: XII, 498 p. 73 illus.
Dimensiuni: 155 x 235 x 27 mm
Greutate: 0.71 kg
Ediția:2013
Editura: Springer Berlin, Heidelberg
Colecția Springer
Seriile Lecture Notes in Computer Science, Theoretical Computer Science and General Issues

Locul publicării:Berlin, Heidelberg, Germany

Public țintă

Research

Cuprins

Invited Talks.- Applying Formal Methods in the Large.- Automating Theorem Proving with SMT.- Certifying Voting Protocols.- Invited Tutorials.-Counterexample Generation Meets Interactive Theorem Proving: Current Results and Future Opportunities.- Canonical Structures for the Working Coq User.- Regular Papers.- MaSh: Machine Learning for Sledgehammer.- Scalable LCF-Style Proof Translation.- Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation.- Automatic Data Refinement.- Data Refinement in Isabelle/HOL.- Light-Weight Containers for Isabelle: Efficient, Extensible, Nestable.- Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1.- Mechanising Turing Machines and Computability Theory in Isabelle/HOL.-A Machine-Checked Proof of the Odd Order Theorem.- Kleene Algebra with Tests and Coq Tools for while Programs.-Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.- Pragmatic Quotient Types in Coq.- Mechanical Verification of SAT Refutations with Extended Resolution.- Formalizing Bounded Increase.- Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types.- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL.- Formal Reasoning about Classified Markov Chains in HOL.- Practical Probability: Applying pGCL to Lattice Scheduling.- Adjustable References.- Handcrafted Inversions Made Operational on Operational Semantics.- Circular Coinduction in Coq Using Bisimulation-Up-To Techniques.- Program Extraction from Nested Definitions.- Subformula Linking as an Interaction Method.- Automatically Generated Infrastructure for De Bruijn Syntaxes.- Shared-Memory Multiprocessing for Interactive Theorem Proving.- A Parallelized Theorem Prover for a Logic with Parallel Execution.- Rough Diamonds.- Communicating Formal Proofs: The Case of Flyspeck.- Square Root and Division Elimination in PVS.- The Picard Algorithm for Ordinary Differential Equations in Coq.- Stateless Higher-OrderLogic with Quantified Types.- Implementing Hash-Consed Structures in Coq.- Towards Certifying Network Calculus.- Steps towards Verified Implementations of HOL Light.

Textul de pe ultima copertă

This book constitutes the refereed proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, held in Rennes, France, in July 2013.
The 26 regular full papers presented together with 7 rough diamond papers, 3 invited talks, and 2 invited tutorials were carefully reviewed and selected from 66 submissions. The papers are organized in topical sections such as program verfication, security, formalization of mathematics and theorem prover development.

Caracteristici

Fast-track conference proceedings of ITP 2013