微信扫一扫,移动浏览光盘
简介
The LNCS series reports state-of-the-art results in computer science research, development, and education, at a high level and in both printed and electronic form. Enjoying tight cooperation with the R&D community,with numerous individuals, as well as with prestigious organizations and societies, LNCS has grown into the most comprehensive computer science research forum available.
The scope of LNCS, including its subseries LNAI, spans the whole range of computer science and information technology including interdisciplinary topics in a variety of application fields. The type of material published traditionally includes
- proceedings (published in time for the respective conference)
- post-proceedings (consisting of thoroughly revised final full papers)
- research m0nographs (which may be based on outstanding PhD work,research projects, technical reports, etc.).
目录
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
Theorem Proving in Higher Order Logics 高阶逻辑中的定理验证
- 名称
- 类型
- 大小
光盘服务联系方式: 020-38250260 客服QQ：4006604884
云图客服：
用户发送的提问，这种方式就需要有位在线客服来回答用户的问题，这种 就属于对话式的,问题是这种提问是否需要用户登录才能提问
Video Player
×
Audio Player
×
pdf Player
×
