Theorem Proving in Higher Order Logics : 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings / edited by Joe Hurd, Tom Melham
(Theoretical Computer Science and General Issues. ISSN:25122029 ; 3603)
データ種別 | 電子ブック |
---|---|
版 | 1st ed. 2005. |
出版者 | (Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer) |
出版年 | 2005 |
大きさ | X, 414 p : online resource |
著者標目 | Hurd, Joe editor Melham, Tom editor SpringerLink (Online service) |
書誌詳細を非表示
一般注記 | 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 This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22–25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?cation. There were 49 papers submitted to TPHOLs 2005 in the full research c- egory, each of which was refereed by at least three reviewers selected by the programcommittee. Of these submissions, 20 researchpapersand 4 proof pearls were accepted for presentation at the conference and publication in this volume. In keeping with longstanding tradition, TPHOLs 2005 also o?ered a venue for the presentation of work in progress, where researchers invited discussion by means of a brief introductory talk and then discussed their work at a poster session. A supplementary proceedings volume was published as a 2005 technical report of the Oxford University Computing Laboratory. The organizers are grateful to Wolfgang Paul and Andrew Pitts for agreeing to give invited talks at TPHOLs 2005 HTTP:URL=https://doi.org/10.1007/11541868 |
---|---|
件 名 | LCSH:Computer science LCSH:Computer systems LCSH:Machine theory LCSH:Software engineering LCSH:Artificial intelligence FREE:Theory of Computation FREE:Computer System Implementation FREE:Formal Languages and Automata Theory FREE:Computer Science Logic and Foundations of Programming FREE:Software Engineering FREE:Artificial Intelligence |
分 類 | LCC:QA75.5-76.95 DC23:004.0151 |
書誌ID | EB00003427 |
ISBN | 9783540318200 |
類似資料
この資料の利用統計
このページへのアクセス回数:14回
※2019年3月27日以降
全貸出数:0回
(1年以内の貸出:0回)
※2019年3月27日以降