最 低 价：￥455.10
定 价：￥568.82
作 者：RichardJ.BoultonPaulB.Jackson 著 著
出 版 社：Oversea Publishing House
出版时间：2001-1-1
I S B N：9783540425250
| Invited Talks JavaCard Program Verification Bart Jacobs View from the Fringe of the Fringe (Joint with CHARME 2001) Steven D. Johnson Using Decision Procedures with a Higher-Order Logic Natarajan Shankar Regular Contributions Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey,Ursula Martin, Sam Owre An Irrational Construction of R from Z Rob D. Arthan HELM and the Semantic Math-Web Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena Caleulational Reasoning Revisited (An Isabelle/Isar Experience) Gertrud Bauer, Markus Wenzel Mechanical Proofs about a Non-repudiation Protocol Giampaolo Bella, Lawrence C. Paulson Proving Hybrid Protocols Correct Mark Biekford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu Nested General Recursion and Partiality in Type Theory Ana Bore, Venanzio Capretta A Higher-Order Calculus for Categories Mario Caccamo, Glynn Winskel Certifying the Fast Fourier Transform with Coq Venanzio Capretta A Generic Library for Floating-Point Numbers and Its Application to Exact Computing Marc Daumas, Laurence Rideau, Laurent Thery Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain Louise A. Dennis, Alan Smaill Abstraction and Refinement in Higher Order Logic Matt Fairtlough, Michael Mendler, Xiaochun Cheng A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL Simon J. Gay Representing Hierarchical Automata in Interactive Theorem Provers Steffen Helke, Florian Kammiiller Refinement Calculus for Logic Programming in Isabelle/HOL David Hemer, Ian Hayes, Paul Strooper Predicate Subtyping with Predicate Sets Joe Hurd A Structural Embedding of Ocsid in PVS Pertti Kellomaki A Certified Polynomial-Based Decision Procedure for Propositional Logic lnmaculada Medina-Bulo, Francisco Palomo-Lozano,Jose A. Alonso-Jimenez Finite Set Theory in ACL2 J Strother Moore The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability) Pavel Naumov, Mark-Oliver Stehr, Jose Meseguer Formalizing Convex Hull Algorithms David Piehardie, Yves Bertot Experiments with Finite Tree Automata in Coq Xavier Rival, Jean Goubault-Larrecq Mizar Light for HOL Light Freek Wiedijk Author Index |
内容加载中，请稍后...
商品评论（0条）