Go to main content

Interactive theorem proving [electronic resource] : 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings / Christian Urban, Xingyuan Zhang (eds.).

ITP (Conference) (6th : 2015 : Nanjing, China); Urban, Christian, editor.; Zhang, Xingyuan, editor.
2015
QA76.9.A96
Available Online
Formats
Format
BibTeX
MARCXML
TextMARC
MARC
DublinCore
EndNote
NLM
RefWorks
RIS
Add to Basket
Cite
Citation

Linked e-resources

Linked Resource
Online Access
Concurrent users
Unlimited
Authorized users
Authorized users
Document Delivery Supplied
Can lend chapters, not whole ebooks

Details

Title
Interactive theorem proving [electronic resource] : 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings / Christian Urban, Xingyuan Zhang (eds.).
Meeting Name
ITP (Conference) (6th : 2015 : Nanjing, China)
ISBN
9783319221021 electronic book
3319221027 electronic book
9783319221014
DOI
https://doi.org/10.1007/978-3-319-22102-1
Published
Cham : Springer, 2015.
Language
English
Description
1 online resource (xi, 469 pages) : illustrations.
Item Number
10.1007/978-3-319-22102-1 doi
Call Number
QA76.9.A96
Dewey Decimal Classification
511.36028563
Summary
This book constitutes the proceedings of the 6th International Conference on Interactive Theorem Proving, ITP 2015, held in Nanjing, China, in August 2015. The 27 papers presented in this volume were carefully reviewed and selected from 54 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.
Note
International conference proceedings.
Includes author index.
Access Note
Access limited to authorized users.
Source of Description
Online resource; title from PDF title page (SpringerLink, viewed August 27, 2015).
Added Author
Urban, Christian, editor.
Zhang, Xingyuan, editor.
Series
Lecture notes in computer science ; 9236.
LNCS sublibrary. SL 1, Theoretical computer science and general issues.
Linked Resources
Online Access
Record Appears in
Online Resources > Ebooks
All Resources
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.

Browse Subjects

Show more subjects...

Statistics

from
to
Export