Type(s) de contenu et mode(s) de consultation : Texte noté : électronique

Auteur(s) : ITP Conférence (6e ; 2015 ; Nanjing, Chine)  Voir les notices liées en tant qu'auteur

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

Publication : Cham : Springer, 2015

Description matérielle : 1 ressource dématérialisée

Collection : Lecture notes in computer science ; 9236
LNCS sublibrary. SL 1, Theoretical computer science and general issues

Note(s) : Titre de l'écran-titre (visionné le 4 mars 2016)
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

Autre(s) auteur(s) : Urban, Christian. Fonction indéterminée  Voir les notices liées en tant qu'auteur
Zhang, Xingyuan. Fonction indéterminée  Voir les notices liées en tant qu'auteur

Autre(s) forme(s) du titre : 
- Autre forme du titre : ITP 2015

Sujet(s) : Génie logiciel  Voir les notices liées en tant que sujet
Informatique  Voir les notices liées en tant que sujet
Algorithmes  Voir les notices liées en tant que sujet
Logique informatique  Voir les notices liées en tant que sujet
Intelligence artificielle  Voir les notices liées en tant que sujet

Indice(s) Dewey :  511.360 28563 (23e éd.) = Démonstration automatique de théorèmes  Voir les notices liées en tant que sujet ; 005.131 (23e éd.) = Logique symbolique (informatique)  Voir les notices liées en tant que sujet

Identifiants, prix et caractéristiques : ISBN 9783319221021

Identifiant de la notice  : ark:/12148/cb44680402h

Notice n° :  FRBNF44680402 (notice reprise d'un réservoir extérieur)

Table des matières : 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 Modula