close
1.

図書

図書
Victor A. Carreño, César A. Muñoz, Sofiène Tahar (eds.)
出版情報: Berlin : Springer, c2002  x, 347 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2410
所蔵情報: loading…
目次情報: 続きを見る
Invited Talks
Formal Methods at NASA Langley / RickyButler
Higher Order Unification 30 Years Later / Gérard Huet
Regular Papers
Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction / Simon J. Ambler ; RoyL. Crole ; Alberto Momigliano
Efficient Reasoning about Executable Specifications in Coq / Gilles Barthe ; Pierre Courtieu
Verified Bytecode Model Checkers / David Basin ; Stefan Friedrich ; Marek Gawkowski
The 5 Colour Theorem in Isabelle/Isar / Gertrud Bauer ; Tobias Nipkow
Type-Theoretic Functional Semantics / Yves Bertot ; Venanzio Capretta ; Kuntal Das Barman
A Proposal for a Formal OCL Semantics in Isabelle/HOL / Achim D. Brucker ; Burkhart Wolff
Explicit Universes for the Calculus of Constructions / Judicaël Courant
Formalised Cut Admissibility for Display Logic / JeremyE. Dawson ; Rajeev GorÆe
Formalizing the Trading Theorem for the Classification of Surfaces / Christophe Dehlinger ; Jean-Francois Dufourd
Free-Style Theorem Proving / David Delahaye
A Comparison of Two Proof Critics: Power vs. Robustness / Louise A. Dennis ; Alan Bundy
Two-Level Meta-reasoning in Coq / AmyP. Felty
PuzzleTool: An Example of Programming Computation and Deduction / Michael J.C. Gordon
A Formal Approach to Probabilistic Termination / Joe Hurd
Using Theorem Proving for Numerical Analysis / Micaela Mayero
Quotient Types: A Modular Approach / AlekseyNogin
Sequent Schema for Derived Rules / Jason Hickey
Algebraic Structures and Dependent Records / Virgile Prevosto ; Damien Doligez ; Therese Hardin
Proving the Equivalence of Microstep and Macrostep Semantics / Klaus Schneider
Weakest Precondition for General Recursive Programs Formalized in Coq / Xingyuan Zhang ; Malcolm Munro ; Mark Harman ; Lin Hu
Author Index
Invited Talks
Formal Methods at NASA Langley / RickyButler
Higher Order Unification 30 Years Later / Gérard Huet
2.

図書

図書
Richard J. Boulton, Paul B. Jackson (eds.)
出版情報: Berlin : Springer, c2001  x, 393 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2152
所蔵情報: loading…
目次情報: 続きを見る
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
Calculational 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 Bickford ; Christoph Kreitz ; Robbert van Renesse ; Xiaoming Liu
Nested General Recursion and Partiality in Type Theory / Ana Bove ; Venanzio Capretta
A Higher-Order Calculus for Categories / Mario Cáccamo ; Glynn Winskel
Certifying the Fast Fourier Transform with Coq
A Generic Library for Floating-Point Numbers and Its Application to Exact Computing / Marc Daumas ; Laurence Rideau ; Laurent Théry
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 Kammüller
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 / Inmaculada Medina-Bulo ; Francisco Palomo-Lozano ; José A. Alonso-Jiménez
Finite Set Theory in ACL2 / J Strother Moore
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability) / Pavel Naumov ; Mark-Oliver Stehr ; José Meseguer
Formalizing Convex Hull Algorithms / David Pichardie ; Yves Bertot
Experiments with Finite Tree Automata in Coq / Xavier Rival ; Jean Goubault-Larrecq
Mizar Light for HOL Light / Freek Wiedijk
Author Index
Invited Talks
JavaCard Program Verification / Bart Jacobs
View from the Fringe of the Fringe (Joint with CHARME 2001) / Steven D. Johnson
3.

図書

図書
Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.)
出版情報: Berlin : Springer, c2004  viii, 336 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 3223
所蔵情報: loading…
目次情報: 続きを見る
Error Analysis of Digital Filters Using Theorem Proving / Behzad Akbarpour ; Sofiène Tahar
Verifying Uniqueness in a Logical Framework / Penny Anderson ; Frank Pfenning
A Program Logic for Resource Verification / David Aspinall ; Lennart Beringer ; Martin Hofmann ; Hans-Wolfgang Loidl ; Alberto Momigliano
Proof Reuse with Extended Inductive Types / Olivier Boite
Hierarchical Reflection / Luís Cruz-Filipe ; Freek Wiedijk
Correct Embedded Computing Futures / Al Davis
Higher Order Rippling in IsaPlanner / Lucas Dixon ; Jacques Fleuriot
A Mechanical Proof of the Cook-Levin Theorem / Ruben Gamboa ; John Cowles
Formalizing the Proof of the Kepler Conjecture / Thomas Hales
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code / Nadeem Abdul Hamid ; Zhong Shao
Extensible Hierarchical Tactic Construction in a Logical Framework / Jason Hickey ; Aleksey Nogin
Theorem Reuse by Proof Term Transformation / Einar Broch Johnsen ; Christoph Lüth
Proving Compatibility Using Refinement / Michael Jones ; Aaron Benson ; Dan Delorey
Java Program Verification via a JVM Deep Embedding in ACL2 / Hanbing Liu ; J. Strother Moore
Reasoning About CBV Functional Programs in Isabelle/HOL / John Longley ; Randy Pollack
Proof Pearl: From Concrete to Functional Unparsing / Jean-Fraçois Monin
A Decision Procedure for Geometry in Coq / Julien Narboux
Recursive Function Definition for Types with Binders / Michael Norrish
Abstractions for Fault-Tolerant Distributed System Verification / Lee Pike ; Jeffrey Maddalon ; Paul Miner ; Alfons Geser
Formalizing Integration Theory with an Application to Probabilistic Algorithms / Stefan Richter
Formalizing Java Dynamic Loading in HOL / Tian-jun Zuo ; Jun-gang Han ; Ping Chen
Certifying Machine Code Safety: Shallow Versus Deep Embedding / Martin Wildmoser ; Tobias Nipkow
Term Algebras with Length Function and Bounded Quantifier Alternation / Ting Zhang ; Henny B. Sipma ; Zohar Manna
Author Index
Error Analysis of Digital Filters Using Theorem Proving / Behzad Akbarpour ; Sofiène Tahar
Verifying Uniqueness in a Logical Framework / Penny Anderson ; Frank Pfenning
A Program Logic for Resource Verification / David Aspinall ; Lennart Beringer ; Martin Hofmann ; Hans-Wolfgang Loidl ; Alberto Momigliano
4.

図書

図書
Jim Grundy, Malcolm Newey (eds.)
出版情報: Berlin ; Tokyo : Springer, c1998  viii, 496 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1479
所蔵情報: loading…
目次情報: 続きを見る
Invited Papers
Verified Lexical Analysis / Tobias Nipkow
Extending Window Inference / Joakim von Wright
Refereed Papers
Program Abstraction in a Higher-Order Logic Framework / Marco Benini ; Sara Kalvala ; Dirk Nowotka
The Village Telephone System: A Case Study in Formal Software Engineering / Karthikeyan Bhargavan ; Carl A. Gunter ; Elsa L. Gunter ; Michael Jackson ; Davor Obradovic ; Pamela Zave
Generating Embeddings from Denotational Descriptions / Richard J. Boulton
An Interface between CLaM and HOL / Richard Boulton ; Konrad Slind ; Alan Bundy ; Mike Gordon
Classical Propositional Decidability via Nuprl Proof Extraction / James L. Caldwell
A Comparison of PVS and Isabelle/HOL / David Griffioen ; Marieke Huisman
Adding External Decision Procedures to HOL90 Securely
Formalizing Basic First Order Model Theory / John Harrison
Formalizing Dijkstra
Mechanical Verification of Total Correctness through
Diversion Verification Conditions / Peter V. Homeier ; David F. Martin
A Type Annotation Scheme for Nuprl / Douglas J. Howe
Verifying a Garbage Collection Algorithm / Paul B. Jackson
Hot: A Concurrent Automated Theorem Prover Based on Higher-Order Tableaux / Karsten Konrad
Free Variables and Subexpressions in Higher-Order Meta Logic / Chuck Liang
An LPO-Based Termination Ordering for Higher-Order Terms without ?-Abstraction / Maxim Lifantsev ; Leo Bachmair
Proving Isomorphism of First-Order Logic Proof Systems in HOL / Anna Mikhajlova
Exploiting Parallelism in Interactive Theorem Provers / Roderick Moten
I/O Automata and Beyond: Temporal Logic and Abstraction in Isabelle / Olaf Müller
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic / Wolfgang Naraschewski ; Markus Wenzel
On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System / Naren Narasimhan ; Ranga Vemuri
Co-inductive Axiomatization of a Synchronous Language / David Nowak ; Jean-Rene Beauvais ; Jean-Pierre Talpin
Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling / François Puitg ; Jean-François Dufourd
A Tool for Data Refinement / Rimvydas RukÃœenas
Mechanizing Relevant Logics with HOL / Hajime Sawamura ; Daisaku Asanuma
Case Studies in Meta-Level Theorem Proving / Friedrich W. von Henke ; Stephan Pfab ; Holger Pfeifer ; Harald Rueß
Formalization of Graph Search Algorithms and Its Applications / Mitsuharu Yamamoto ; Koichi Takahashi ; Masami Hagiya ; Shin-ya Nishizaki ; Tetsuo Tamai
Author Index
Invited Papers
Verified Lexical Analysis / Tobias Nipkow
Extending Window Inference / Joakim von Wright
5.

図書

図書
Mark Aagaard, John Harrison (eds.)
出版情報: Berlin : Springer, c2000  ix, 533 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1869
所蔵情報: loading…
6.

図書

図書
Yves Bertot ... [et al.] (eds.)
出版情報: Berlin : Springer, c1999  viii, 358 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1690
所蔵情報: loading…
7.

図書

図書
David Basin, Burkhart Wolff (eds.)
出版情報: Berlin ; Tokyo : Springer, c2003  x, 366 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 2758
所蔵情報: loading…
8.

図書

図書
Elsa L. Gunter, Amy Felty (eds.)
出版情報: Berlin ; Heidelberg : Springer, c1997  viii, 337 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1275
所蔵情報: loading…
9.

図書

図書
J. von Wright, J. Grundy, J. Harrison, (eds.)
出版情報: Berlin ; Tokyo : Springer, c1996  viii, 446 p. ; 24 cm
シリーズ名: Lecture notes in computer science ; 1125
所蔵情報: loading…
文献の複写および貸借の依頼を行う
 文献複写・貸借依頼