Theorem Proving in Higher Order Logics
Editat de Joe Hurd, Tom Melhamen Limba Engleză Paperback – 8 aug 2005
Preț: 327.49 lei
Preț vechi: 409.37 lei
-20% Nou
Puncte Express: 491
Preț estimativ în valută:
57.95€ • 67.58$ • 50.88£
57.95€ • 67.58$ • 50.88£
Carte tipărită la comandă
Livrare economică 16-30 ianuarie 26
Preluare comenzi: 021 569.72.76
Specificații
ISBN-13: 9783540283720
ISBN-10: 3540283722
Pagini: 424
Ilustrații: X, 414 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540283722
Pagini: 424
Ilustrații: X, 414 p.
Dimensiuni: 155 x 235 x 23 mm
Greutate: 0.64 kg
Ediția:2005
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
Public țintă
ResearchCuprins
Invited Papers.- On the Correctness of Operating System Kernels.- Alpha-Structural Recursion and Induction.- Regular Papers.- Shallow Lazy Proofs.- Mechanized Metatheory for the Masses: The PoplMark Challenge.- A Structured Set of Higher-Order Problems.- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS.- Proving Equalities in a Commutative Ring Done Right in Coq.- A HOL Theory of Euclidean Space.- A Design Structure for Higher Order Quotients.- Axiomatic Constructor Classes in Isabelle/HOLCF.- Meta Reasoning in ACL2.- Reasoning About Java Programs with Aliasing and Frame Conditions.- Real Number Calculations and Theorem Proving.- Verifying a Secure Information Flow Analyzer.- Proving Bounds for Real Linear Programs in Isabelle/HOL.- Essential Incompleteness of Arithmetic Verified by Coq.- Verification of BDD Normalization.- Extensionality in the Calculus of Constructions.- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic.- A Generic Network on Chip Model.- Formal Verification of a SHA-1 Circuit Core Using ACL2.- From PSL to LTL: A Formal Validation in HOL.- Proof Pearls.- Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2.- Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2.- Proof Pearl: Defining Functions over Finite Sets.- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.