단행본 상세

서지주요정보
Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings
서명 / 저자 Theorem Proving in Higher Order Logics [electronic resource] : 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings / edited by David Basin, Burkhart Wolff.
저자명 Basin, David. editor. edt http://id.loc.gov/vocabulary/relators/edt ; Wolff, Burkhart. editor. edt http://id.loc.gov/vocabulary/relators/edt
단체명 SpringerLink (Online service)
판사항 1st ed. 2003.
발행사항 Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2003.
총서명 Lecture Notes in Computer Science, 1611-3349 ; 2758
Online Access https://doi.org/10.1007/b11935 URL

서지기타정보

서지기타정보
ISBN 9783540451303
기타 표준번호 10.1007/b11935
청구기호 B1-5802
형태사항 X, 366 p. online resource.
언어 English
내용 Invited Talk I -- Click’n Prove: Interactive Proofs within Set Theory -- Hardware and Assembler Languages -- Formal Specification and Verification of ARM6 -- A Programming Logic for Java Bytecode Programs -- Verified Bytecode Subroutines -- Proof Automation I -- Complete Integer Decision Procedures as Derived Rules in HOL -- Changing Data Representation within the Coq System -- Applications of Polytypism in Theorem Proving -- Proof Automation II -- A Coverage Checking Algorithm for LF -- Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions -- Tool Combination -- Embedding of Systems of Affine Recurrence Equations in Coq -- Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover -- Combining Testing and Proving in Dependent Type Theory -- Invited Talk II -- Reasoning about Proof Search Specifications: An Abstract -- Logic Extensions -- Program Extraction from Large Proof Developments -- First Order Logic with Domain Conditions -- Extending Higher-Order Unification to Support Proof Irrelevance -- Advances in Theorem Prover Technology -- Inductive Invariants for Nested Recursion -- Implementing Modules in the Coq System -- MetaPRL – A Modular Logical Environment -- Mathematical Theories -- Proving Pearl: Knuth’s Algorithm for Prime Numbers -- Formalizing Hilbert’s Grundlagen in Isabelle/Isar -- Security -- Using Coq to Verify Java CardTM Applet Isolation Properties -- Verifying Second-Level Security Protocols.
주제 Philosophy.
Machine theory.
Logic design.
Software engineering.
Computer science.
Artificial intelligence.
Philosophy.
Formal Languages and Automata Theory.
Logic Design.
Software Engineering.
Computer Science Logic and Foundations of Programming.
Artificial Intelligence.
보유판 및 특별호 저록 Springer Nature eBook
Printed edition: 9783662199480 Printed edition: 9783540406648
QR CODE