國立虎尾科技大學 |

Interactive theorem proving = 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017 : proceedings /

紀錄類型:	書目-語言資料,印刷品 : Monograph/item
正題名/作者:	Interactive theorem proving/ edited by Mauricio Ayala-Rincon, Cesar A. Munoz.
其他題名:	8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017 : proceedings /
其他題名:	ITP 2017
其他作者:	Ayala-Rincon, Mauricio.
團體作者:	Workshop on the Preservation of Stability under Discretization
出版者:	Cham :Springer International Publishing : : 2017.,
面頁冊數:	xix, 532 p. :ill., digital ; : 24 cm.;
Contained By:	Springer eBooks
標題:	Automatic theorem proving - Congresses. -
電子資源:	http://dx.doi.org/10.1007/978-3-319-66107-0
ISBN:	9783319661070

Interactive theorem proving = 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017 : proceedings /
Interactive theorem proving8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017 : proceedings /[electronic resource] :ITP 2017edited by Mauricio Ayala-Rincon, Cesar A. Munoz. - Cham :Springer International Publishing :2017. - xix, 532 p. :ill., digital ;24 cm. - Lecture notes in computer science,104990302-9743 ;. - Lecture notes in computer science ;6140..

Whitebox Automation -- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System -- Automating Formalization by Statistical and Semantic Parsing of Mathematics -- A Formalization of Convex Polyhedra Based on the Simplex Method -- A Formal Proof of the Expressiveness of Deep Learning -- Formalization of the Lindemann-Weierstrass Theorem -- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics -- Formal Verification of a Floating-Point Expansion Renormalization Algorithm -- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation -- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability -- A Formal Proof in Coq of LaSalle's Invariance Principle -- How to Get More out of Your Oracles -- Certifying Standard and Stratified Datalog Inference Engines in SSReect -- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq -- Bellerophon: Tactical Theorem Proving for Hybrid Systems -- Formalizing Basic Quaternionic Analysis -- A Formalized General Theory of Syntax with Bindings -- Proof Certificates in PVS -- Efficient, Verified Checking of Propositional Proofs -- Proof Tactics for Assertions in Separation Logic -- Categoricity Results for Second-Order ZF in Dependent Type Theory -- Making PVS Accessible to Generic Services by Interpretation in a Universal Format -- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics -- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms -- Typing Total Recursive Functions in Coq -- Effect Polymorphism in Higher-Order Logic (Proof Pearl) -- Schulze Voting as Evidence Carrying Computation -- Verified Spilling and Translation Validation with Repair -- A Verified Generational Garbage Collector for CakeML -- A Formalisation of Consistent Consequence for Boolean Equation Systems -- Homotopy Type Theory in Lean -- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology -- Formalization of the Fundamental Group in Untyped Set Theory Using auto2.

This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017. The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories.

ISBN: 9783319661070

Standard No.: 10.1007/978-3-319-66107-0doiSubjects--Topical Terms:

665433
Automatic theorem proving
--Congresses.

LC Class. No.: QA76.9.A96

Dewey Class. No.: 511.36028563

Interactive theorem proving = 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017 : proceedings /
LDR:03725nam a2200349 a 4500 001 923510
003 DE-He213
005 20170820174224.0
006 m d
007 cr nn 008maaau
008 190625s2017 gw s 0 eng d
020 $a 9783319661070 $q (electronic bk.)
020 $a 9783319661063 $q (paper)
024 7 $a 10.1007/978-3-319-66107-0 $2 doi
035 $a 978-3-319-66107-0
040 $a GP $c GP
041 0 $a eng
050 4 $a QA76.9.A96
072 7 $a UYA $2 bicssc
072 7 $a MAT018000 $2 bisacsh
072 7 $a COM051010 $2 bisacsh
082 0 4 $a 511.36028563 $2 23
090 $a QA76.9.A96 $b I89 2017
111 2 $a Workshop on the Preservation of Stability under Discretization $d (2001 : $c Fort Collins, Colo.) $3 527686
245 1 0 $a Interactive theorem proving $h [electronic resource] : $b 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017 : proceedings / $c edited by Mauricio Ayala-Rincon, Cesar A. Munoz.
246 3 $a ITP 2017
260 $a Cham : $c 2017. $b Springer International Publishing : $b Imprint: Springer,
300 $a xix, 532 p. : $b ill., digital ; $c 24 cm.
490 1 $a Lecture notes in computer science, $x 0302-9743 ; $v 10499
505 0 $a Whitebox Automation -- Automated Theory Exploration for Interactive Theorem Proving: An Introduction to the Hipster System -- Automating Formalization by Statistical and Semantic Parsing of Mathematics -- A Formalization of Convex Polyhedra Based on the Simplex Method -- A Formal Proof of the Expressiveness of Deep Learning -- Formalization of the Lindemann-Weierstrass Theorem -- CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics -- Formal Verification of a Floating-Point Expansion Renormalization Algorithm -- How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation -- FoCaLiZe and Dedukti to the Rescue for Proof Interoperability -- A Formal Proof in Coq of LaSalle's Invariance Principle -- How to Get More out of Your Oracles -- Certifying Standard and Stratified Datalog Inference Engines in SSReect -- Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq -- Bellerophon: Tactical Theorem Proving for Hybrid Systems -- Formalizing Basic Quaternionic Analysis -- A Formalized General Theory of Syntax with Bindings -- Proof Certificates in PVS -- Efficient, Verified Checking of Propositional Proofs -- Proof Tactics for Assertions in Separation Logic -- Categoricity Results for Second-Order ZF in Dependent Type Theory -- Making PVS Accessible to Generic Services by Interpretation in a Universal Format -- Formally Verified Safe Vertical Maneuvers for Non-Deterministic, Accelerating Aircraft Dynamics -- Using Abstract Stobjs in ACL2 to Compute Matrix Normal Forms -- Typing Total Recursive Functions in Coq -- Effect Polymorphism in Higher-Order Logic (Proof Pearl) -- Schulze Voting as Evidence Carrying Computation -- Verified Spilling and Translation Validation with Repair -- A Verified Generational Garbage Collector for CakeML -- A Formalisation of Consistent Consequence for Boolean Equation Systems -- Homotopy Type Theory in Lean -- Verifying a Concurrent Garbage Collector Using a Rely-Guarantee Methodology -- Formalization of the Fundamental Group in Untyped Set Theory Using auto2.
520 $a This book constitutes the refereed proceedings of the 8th International Conference on Interactive Theorem Proving, ITP 2017, held in Brasilia, Brazil, in September 2017. The 28 full papers, 2 rough diamond papers, and 3 invited talk papers presented were carefully reviewed and selected from 65 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematical theories.
650 0 $a Automatic theorem proving $v Congresses. $3 665433 $3 727761
650 0 $a Software engineering $v Congresses. $3 528500
650 1 4 $a Computer Science. $3 593922
650 2 4 $a Mathematical Logic and Formal Languages. $3 670059
650 2 4 $a Logics and Meanings of Programs. $3 670058
650 2 4 $a System Performance and Evaluation. $3 669346
650 2 4 $a Software Engineering. $3 669632
650 2 4 $a Programming Languages, Compilers, Interpreters. $3 669782
650 2 4 $a Artificial Intelligence (incl. Robotics) $3 593924
700 1 $a Ayala-Rincon, Mauricio. $3 1199873
700 1 $a Munoz, Cesar A. $3 1199874
710 2 $a SpringerLink (Online service) $3 593884
773 0 $t Springer eBooks
830 0 $a Lecture notes in computer science ; $v 6140. $3 744199
856 4 0 $u http://dx.doi.org/10.1007/978-3-319-66107-0
950 $a Computer Science (Springer-11645)