Please use this identifier to cite or link to this item:
http://localhost/handle/Hannan/1534
Full metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor | ITP (Conference) ; (8th : ; 2017 : ; Braselia, Brazil) ; | en_US |
| dc.contributor.author | Ayala-Rincen, M. ; (Mauricio), ; editor ; | en_US |
| dc.contributor.author | Mueoz, Cesar A., ; 1968- ; editor ; | en_US |
| dc.date.accessioned | 2013 | en_US |
| dc.date.accessioned | 2020-05-17T08:29:34Z | - |
| dc.date.available | 2020-05-17T08:29:34Z | - |
| dc.date.issued | 2017 | en_US |
| dc.identifier.isbn | 9783319661070 ; (electronic bk.) ; | en_US |
| dc.identifier.isbn | 3319661078 ; (electronic bk.) ; | en_US |
| dc.identifier.isbn | 9783319661063 ; (print) ; | en_US |
| dc.identifier.isbn | 331966106X ; | en_US |
| dc.identifier.uri | http://localhost/handle/Hannan/1534 | - |
| dc.description | en_US | |
| dc.description | Available to OhioLINK libraries ; | en_US |
| dc.description | en_US | |
| dc.description | Ohio Library and Information Network ; | en_US |
| dc.description | en_US | |
| dc.description | Printed edition: ; 9783319661063 ; | en_US |
| dc.description.abstract | 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 ; | en_US |
| dc.description.statementofresponsibility | Mauricio Ayala-Rincen, Cesar A. Mueoz (eds.) | en_US |
| dc.description.tableofcontents | 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 ; | en_US |
| dc.format.extent | 1 online resource (xix, 532 pages) : ; illustrations ; | en_US |
| dc.format.extent | International conference proceedings ; | en_US |
| dc.format.extent | Includes author index ; | en_US |
| dc.publisher | Springer, | en_US |
| dc.relation.ispartofseries | Lecture notes in computer science, ; 0302-9743 ; ; 10499 ; | en_US |
| dc.relation.ispartofseries | LNCS sublibrary., SL 1, Theoretical computer science and general issues ; | en_US |
| dc.relation.ispartofseries | Lecture notes in computer science ; ; 10499. ; 0302-9743 ; | en_US |
| dc.relation.ispartofseries | LNCS sublibrary. ; SL 1, ; Theoretical computer science and general issues ; | en_US |
| dc.relation.haspart | 9783319661070.pdf | en_US |
| dc.subject | Automatic theorem proving ; Congresses ; | en_US |
| dc.subject | Software engineering ; Congresses ; | en_US |
| dc.title | Interactive theorem proving : | en_US |
| dc.title.alternative | 8th International Conference, ITP 2017, Braselia, Brazil, September 26-29, 2017, Proceedings / | en_US |
| dc.title.alternative | ITP 2017 ; | en_US |
| dc.type | Book | en_US |
| dc.publisher.place | Cham, Switzerland : | en_US |
| dc.classification.lc | QA76.9.A96 ; | en_US |
| Appears in Collections: | مهندسی فناوری اطلاعات | |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 9783319661070.pdf | 15.71 MB | Adobe PDF |  Preview File |
Full metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor | ITP (Conference) ; (8th : ; 2017 : ; Braselia, Brazil) ; | en_US |
| dc.contributor.author | Ayala-Rincen, M. ; (Mauricio), ; editor ; | en_US |
| dc.contributor.author | Mueoz, Cesar A., ; 1968- ; editor ; | en_US |
| dc.date.accessioned | 2013 | en_US |
| dc.date.accessioned | 2020-05-17T08:29:34Z | - |
| dc.date.available | 2020-05-17T08:29:34Z | - |
| dc.date.issued | 2017 | en_US |
| dc.identifier.isbn | 9783319661070 ; (electronic bk.) ; | en_US |
| dc.identifier.isbn | 3319661078 ; (electronic bk.) ; | en_US |
| dc.identifier.isbn | 9783319661063 ; (print) ; | en_US |
| dc.identifier.isbn | 331966106X ; | en_US |
| dc.identifier.uri | http://localhost/handle/Hannan/1534 | - |
| dc.description | en_US | |
| dc.description | Available to OhioLINK libraries ; | en_US |
| dc.description | en_US | |
| dc.description | Ohio Library and Information Network ; | en_US |
| dc.description | en_US | |
| dc.description | Printed edition: ; 9783319661063 ; | en_US |
| dc.description.abstract | 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 ; | en_US |
| dc.description.statementofresponsibility | Mauricio Ayala-Rincen, Cesar A. Mueoz (eds.) | en_US |
| dc.description.tableofcontents | 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 ; | en_US |
| dc.format.extent | 1 online resource (xix, 532 pages) : ; illustrations ; | en_US |
| dc.format.extent | International conference proceedings ; | en_US |
| dc.format.extent | Includes author index ; | en_US |
| dc.publisher | Springer, | en_US |
| dc.relation.ispartofseries | Lecture notes in computer science, ; 0302-9743 ; ; 10499 ; | en_US |
| dc.relation.ispartofseries | LNCS sublibrary., SL 1, Theoretical computer science and general issues ; | en_US |
| dc.relation.ispartofseries | Lecture notes in computer science ; ; 10499. ; 0302-9743 ; | en_US |
| dc.relation.ispartofseries | LNCS sublibrary. ; SL 1, ; Theoretical computer science and general issues ; | en_US |
| dc.relation.haspart | 9783319661070.pdf | en_US |
| dc.subject | Automatic theorem proving ; Congresses ; | en_US |
| dc.subject | Software engineering ; Congresses ; | en_US |
| dc.title | Interactive theorem proving : | en_US |
| dc.title.alternative | 8th International Conference, ITP 2017, Braselia, Brazil, September 26-29, 2017, Proceedings / | en_US |
| dc.title.alternative | ITP 2017 ; | en_US |
| dc.type | Book | en_US |
| dc.publisher.place | Cham, Switzerland : | en_US |
| dc.classification.lc | QA76.9.A96 ; | en_US |
| Appears in Collections: | مهندسی فناوری اطلاعات | |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 9783319661070.pdf | 15.71 MB | Adobe PDF | Preview File |
Full metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor | ITP (Conference) ; (8th : ; 2017 : ; Braselia, Brazil) ; | en_US |
| dc.contributor.author | Ayala-Rincen, M. ; (Mauricio), ; editor ; | en_US |
| dc.contributor.author | Mueoz, Cesar A., ; 1968- ; editor ; | en_US |
| dc.date.accessioned | 2013 | en_US |
| dc.date.accessioned | 2020-05-17T08:29:34Z | - |
| dc.date.available | 2020-05-17T08:29:34Z | - |
| dc.date.issued | 2017 | en_US |
| dc.identifier.isbn | 9783319661070 ; (electronic bk.) ; | en_US |
| dc.identifier.isbn | 3319661078 ; (electronic bk.) ; | en_US |
| dc.identifier.isbn | 9783319661063 ; (print) ; | en_US |
| dc.identifier.isbn | 331966106X ; | en_US |
| dc.identifier.uri | http://localhost/handle/Hannan/1534 | - |
| dc.description | en_US | |
| dc.description | Available to OhioLINK libraries ; | en_US |
| dc.description | en_US | |
| dc.description | Ohio Library and Information Network ; | en_US |
| dc.description | en_US | |
| dc.description | Printed edition: ; 9783319661063 ; | en_US |
| dc.description.abstract | 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 ; | en_US |
| dc.description.statementofresponsibility | Mauricio Ayala-Rincen, Cesar A. Mueoz (eds.) | en_US |
| dc.description.tableofcontents | 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 ; | en_US |
| dc.format.extent | 1 online resource (xix, 532 pages) : ; illustrations ; | en_US |
| dc.format.extent | International conference proceedings ; | en_US |
| dc.format.extent | Includes author index ; | en_US |
| dc.publisher | Springer, | en_US |
| dc.relation.ispartofseries | Lecture notes in computer science, ; 0302-9743 ; ; 10499 ; | en_US |
| dc.relation.ispartofseries | LNCS sublibrary., SL 1, Theoretical computer science and general issues ; | en_US |
| dc.relation.ispartofseries | Lecture notes in computer science ; ; 10499. ; 0302-9743 ; | en_US |
| dc.relation.ispartofseries | LNCS sublibrary. ; SL 1, ; Theoretical computer science and general issues ; | en_US |
| dc.relation.haspart | 9783319661070.pdf | en_US |
| dc.subject | Automatic theorem proving ; Congresses ; | en_US |
| dc.subject | Software engineering ; Congresses ; | en_US |
| dc.title | Interactive theorem proving : | en_US |
| dc.title.alternative | 8th International Conference, ITP 2017, Braselia, Brazil, September 26-29, 2017, Proceedings / | en_US |
| dc.title.alternative | ITP 2017 ; | en_US |
| dc.type | Book | en_US |
| dc.publisher.place | Cham, Switzerland : | en_US |
| dc.classification.lc | QA76.9.A96 ; | en_US |
| Appears in Collections: | مهندسی فناوری اطلاعات | |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 9783319661070.pdf | 15.71 MB | Adobe PDF | Preview File |