Theorem Proving in Higher Order Logics
Editat de Elsa L. Gunter, Amy Feltyen Limba Engleză Paperback – 6 aug 1997
The volume presents 19 carefully revised full papers selected from 32 submissions during a thorough reviewing process. The papers cover work related to all aspects of theorem proving in higher order logics, particularly based on secure mechanization of those logics; the theorem proving systems addressed include Coq, HOL, Isabelle, LEGO, and PVS.
Preț: 325.03 lei
Preț vechi: 406.29 lei
-20%
Puncte Express: 488
Carte tipărită la comandă
Livrare economică 14-28 iulie
Livrare prin curier în România Termenul estimat este afișat lângă disponibilitate.
Transport gratuit de la 400.00 lei Plată online sau ramburs, în funcție de opțiunile comenzii.
Retur gratuit în 14 zile Comandă securizată și suport în română.
Specificații
ISBN-13: 9783540633792
ISBN-10: 3540633790
Pagini: 356
Ilustrații: X, 346 p.
Dimensiuni: 155 x 235 x 20 mm
Greutate: 0.54 kg
Ediția:1997
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
ISBN-10: 3540633790
Pagini: 356
Ilustrații: X, 346 p.
Dimensiuni: 155 x 235 x 20 mm
Greutate: 0.54 kg
Ediția:1997
Editura: Springer
Locul publicării:Berlin, Heidelberg, Germany
V-ar putea interesa
-
Perspectives of Information SystemsVesa SavolainenPreț: 379.51 lei -
-18%Preț: 1422.96 lei1735.32 lei -
UML for RealLuciano Lavagno-20%Preț: 960.14 lei1200.18 lei -
The Basics of Line Balancing and JIT KittingBeverly TownsendPreț: 209.66 lei -
Capacity Management in MRP, APS & S&op SoftwareShaun SnappPreț: 328.86 lei -
High Performance ComputingMichela Taufer-20%Preț: 343.68 lei429.60 lei -
Computer Performance EngineeringDieter Fiems-20%Preț: 319.10 lei398.88 lei -
-20%Preț: 316.03 lei395.04 lei -
Tools for High Performance Computing 2016Christoph Niethammer-20%Preț: 616.43 lei770.54 lei -
Evolvable Systems: From Biology to HardwareJ. Manuel Moreno-20%Preț: 319.28 lei399.10 lei -
-20%Preț: 327.84 lei409.80 lei -
-20%Preț: 316.43 lei395.54 lei -
Algorithmen und Datenstrukturen im VLSI-DesignChristoph Meinel-20%Preț: 349.93 lei437.41 lei -
Model Driven Architecture - Foundations and ApplicationsDavid Akehurst-20%Preț: 318.69 lei398.37 lei -
-20%Preț: 326.24 lei407.80 lei -
Data-oriented ReengineeringJörg P. Wadsack-20%Preț: 528.92 lei661.14 lei -
InternetwareHong Mei-20%Preț: 646.12 lei807.65 lei
Public țintă
ResearchCuprins
An Isabelle-based theorem prover for VDM-SL.- Executing formal specifications by translation to higher order logic programming.- Human-style theorem proving using PVS.- A hybrid approach to verifying liveness in a symmetric multi-processor.- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis.- ML programming in constructive type theory.- Possibly infinite sequences in theorem provers: A comparative study.- Proof normalization for a first-order formulation of higher-order logic.- Using a PVS embedding of CSP to verify authentication protocols.- Verifying the accuracy of polynomial approximations in HOL.- A full formalisation of ?-calculus theory in the calculus of constructions.- Rewriting, decision procedures and lemma speculation for automated hardware verification.- Refining reactive systems in HOL using action systems.- On formalization of bicategory theory.- Towards an object-oriented progification language.- Verification for robust specification.- A theory of structured model-based specifications in Isabelle/HOL.- Proof presentation for Isabelle.- Derivation and use of induction schemes in higher-order logic.- Higher order quotients and their implementation in Isabelle HOL.- Type classes and overloading in higher-order logic.- A comparative study of Coq and HOL.