Interactive theorem proving : 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings /: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings. (2015)

• Record Type: Book
• Other Titles: ITP 2015
• Further Information: Note: Christian Urban, Xingyuan Zhang (eds.).
• Editors: Urban, Christian; Zhang, Xingyuan
• Other Names: ITP (Conference), 6th
• Contents: Verified, Practical Upper Bounds for State Space Diameters -- Formalization of Error-correcting Codes: from Hamming to Modern Coding Theory -- ROSCoq: Robots powered by Constructive Reals -- Asynchronous processing of Coq documents: from the kernel up to the user interface -- A Concrete Memory Model for CompCert -- Validating Dominator Trees for a Fast, Verified Dominance Test -- Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra -- Mechanisation of AKS Algorithm -- Machine-Checked Verification of the Correctness and Amortized -- Improved Tool Support for Machine-Code Decompilation in HOL4 -- A Formalized Hierarchy of Probabilistic System Types -- Learning To Parse on Aligned Corpora -- A Consistent Foundation for Isabelle/HOL -- Foundational Property-Based Testing -- A First-Order Functional Intermediate Language for Verified Compilers -- Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions -- ModuRes: a Coq Library for Modular Reasoning about Concurrent -- Higher-Order Imperative Programming Languages -- Transfinite Constructions in Classical Type Theory -- A Mechanized Theory of regular trees in dependent type theory -- Deriving Comparators and Show-Functions in Isabelle/HOL -- Formalizing Knot Theory in Isabelle/HOL -- Pattern Matches in HOL: A New Representation and Improved Code Generation.
• Publisher Details: Cham : Springer
• Publication Date: 2015
• Extent: 1 online resource (xi, 469 pages), illustrations
• Subjects: 511.36028563; Computer science; Automatic theorem proving -- Congresses; Logic, Symbolic and mathematical -- Congresses; Automatic theorem proving; Logic, Symbolic and mathematical; Mathematical Theory; Mathematics; Physical Sciences & Mathematics; Computers -- Intelligence (AI) & Semantics; Computers -- Programming -- General; Computers -- Software Development & Engineering -- General; Computers -- Security -- General; Computers -- Programming -- Algorithms; Artificial intelligence; Computer programming / software development; Software Engineering; Computer security; Algorithms & data structures; Artificial intelligence; Logic design; Software engineering; Computer security; Computer software; Mathematics -- Logic; Mathematical theory of computation; Electronic books; Conference papers and proceedings; Electronic books
• Languages: English
• ISBNs: 9783319221021; 3319221027; 3319221019; 9783319221014
• Related ISBNs: 9783319221014
• Notes: Note: Online resource; title from PDF title page (SpringerLink, viewed August 27, 2015).
• Access Rights: Legal Deposit; Only available on premises controlled by the deposit library and to one user at any one time; The Legal Deposit Libraries (Non-Print Works) Regulations (UK).
• Access Usage: Restricted: Printing from this resource is governed by The Legal Deposit Libraries (Non-Print Works) Regulations (UK) and UK copyright law currently in force.