Theorem proving in higher order logics : 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002 : proceedings /
This book constitutes the refereed proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, held in Hampton, VA, USA in August 2002. The 20 revised full papers presented together with 2 invited contributions were carefully reviewed and selected from 34...
| Corporate Author: | |
|---|---|
| Other Authors: | , , |
| Format: | Conference Proceeding Book |
| Language: | English |
| Published: |
Berlin ; New York :
Springer,
c2002
Berlin ; New York : ©2002 |
| Series: | Lecture notes in computer science ;
2410 Lecture notes in computer science Lecture notes in artificial intelligence. |
| Subjects: |
| LEADER | 09086nam a22010214a 4500 | ||
|---|---|---|---|
| 001 | e6334b4f-e7e4-4c80-83a5-e1caaacda7a3 | ||
| 005 | 20240926000000.0 | ||
| 008 | 020716s2002 gw a b 101 0 eng | ||
| 010 | |a 2002029204 | ||
| 010 | |a 2002029204 | ||
| 015 | |a GBA2-73216 | ||
| 019 | |a 166466497 |a 729901535 |a 768064085 |a 990467363 |a 1005828364 |a 1044473114 | ||
| 020 | |a 3540440399 (pbk. : alk. paper) | ||
| 020 | |a 3540440399 |q paperback |q alkaline paper | ||
| 020 | |a 3540456856 |q (electronic bk.) | ||
| 020 | |a 9783540456858 |q (electronic bk.) | ||
| 020 | |z 3540440399 | ||
| 020 | |z 9783540440390 | ||
| 024 | 7 | |a 10.1007/3-540-45685-6 |2 doi | |
| 035 | |a (MCM)001122567MIT01 | ||
| 035 | |a (NcD)003127482DUK01 | ||
| 035 | |a (OCoLC)50252017 | ||
| 035 | |a (OCoLC)50393706 |z (OCoLC)166466497 |z (OCoLC)729901535 |z (OCoLC)768064085 |z (OCoLC)990467363 |z (OCoLC)1005828364 |z (OCoLC)1044473114 | ||
| 035 | |a 50252017 | ||
| 035 | |a spocm50393706 | ||
| 035 | |l (OCoLC)50393706 | ||
| 040 | |a COO |b eng |e pn |c COO |d HNK |d BAKER |d QCL |d OCLCQ |d YNG |d OCLCQ |d DKDLA |d OCLCQ |d OCLCO |d OCLCQ |d GW5XE |d OCLCA |d OCLCF |d OCLCQ |d OCLCO |d OCLCQ |d UA@ |d OCL |d OCLCO |d OCLCQ |d YDX |d LIP |d UAB |d ESU |d OCLCQ |d VT2 |d BUF |d OCLCA |d LEAUB |d OL$ |d OCLCQ |d UKAHL |d OCLCO |d OCLCQ |d OCLCO |d WSU |d OCLCO |d OCLCL |d CSt | ||
| 040 | |a DLC |b eng |c DLC |d CQ |d OHX |d C#P |d NDD | ||
| 040 | |a DLC |c DLC |d C$Q |d OHX |d C#P |d UKM |d MYG |d OrLoB-B | ||
| 042 | |a pcc | ||
| 049 | |a MYGG | ||
| 050 | 4 | |a QA76.9.A96 |b T655 2002 | |
| 050 | 0 | 0 | |a QA76.9.A96 |b T655 2002 |
| 050 | 9 | 9 | |a QA75.5 |b .L438 v.2410 |
| 072 | 7 | |a COM032000 |2 bisacsh | |
| 072 | 7 | |a COM067000 |2 bisacsh | |
| 072 | 7 | |a QA |2 lcco | |
| 072 | 7 | |a UYD |2 bicssc | |
| 082 | 0 | 0 | |a 004/.01/5113 |2 21 |
| 082 | 0 | 4 | |a 004/.01/5113 |2 21 |
| 092 | |a 001.64 |b L471, v. 2410 | ||
| 099 | |a QA76.9.A96.I577 2002 | ||
| 111 | 2 | |a TPHOLs |n (15th : |d 2002 : |c Hampton, Va.) | |
| 245 | 1 | 0 | |a Theorem proving in higher order logics : |b 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002 : proceedings / |c Victor A. Carreño, César A. Muñoz, Sofiène Tahar, eds |
| 260 | |a Berlin ; |a New York : |b Springer, |c c2002 | ||
| 260 | |a Berlin ; |a New York : |b Springer, |c ©2002 | ||
| 300 | |a 1 online resource (x, 347 pages) : |b illustrations | ||
| 300 | |a x, 347 p. : |b ill. ; |c 24 cm | ||
| 336 | |a text |b txt |2 rdacontent | ||
| 337 | |a computer |b c |2 rdamedia | ||
| 337 | |a unmediated |b n |2 rdamedia | ||
| 338 | |a online resource |b cr |2 rdacarrier | ||
| 338 | |a volume |b nc |2 rdacarrier | ||
| 347 | |a text file |2 rdaft | ||
| 347 | |a text file |b PDF |2 rda | ||
| 490 | 1 | |a Lecture notes in computer science, |x 0302-9743 ; |v 2410 |a Lecture notes in artifical intelligence | |
| 490 | 1 | |a Lecture notes in computer science, |x 0302-9743 ; |v 2410 |a Lecture notes in artificial intelligence | |
| 504 | |a Includes bibliographical references and index | ||
| 505 | 0 | |a Invited Talks -- Formal Methods at NASA Langley -- Higher Order Unification 30 Years Later -- Regular Papers -- Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction -- Efficient Reasoning about Executable Specifications in Coq -- Verified Bytecode Model Checkers -- The 5 Colour Theorem in Isabelle/Isar -- Type-Theoretic Functional Semantics -- A Proposal for a Formal OCL Semantics in Isabelle/HOL -- Explicit Universes for the Calculus of Constructions -- Formalised Cut Admissibility for Display Logic -- Formalizing the Trading Theorem for the Classification of Surfaces -- Free-Style Theorem Proving -- A Comparison of Two Proof Critics: Power vs. Robustness -- Two-Level Meta-reasoning in Coq -- PuzzleTool: An Example of Programming Computation and Deduction -- A Formal Approach to Probabilistic Termination -- Using Theorem Proving for Numerical Analysis Correctness Proof of an Automatic Differentiation Algorithm -- Quotient Types: A Modular Approach -- Sequent Schema for Derived Rules -- Algebraic Structures and Dependent Records -- Proving the Equivalence of Microstep and Macrostep Semantics -- Weakest Precondition for General Recursive Programs Formalized in Coq | |
| 505 | 0 | 0 | |t Formal Methods at NASA Langley / |r Ricky Butler -- |t Higher Order Unification 30 Years Later / |r Gerard Huet -- |t Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction / |r Simon J. Ambler, Roy L. Crole and Alberto Momigliano -- |t Efficient Reasoning about Executable Specifications in Coq / |r Gilles Barthe and Pierre Courtieu -- |t Verified Bytecode Model Checkers / |r David Basin, Stefan Friedrich and Marek Gawkowski -- |t The 5 Colour Theorem in Isabelle/Isar / |r Gertrud Bauer and Tobias Nipkow -- |t Type-Theoretic Functional Semantics / |r Yves Bertot, Venanzio Capretta and Kuntal Das Barman -- |t A Proposal for a Formal OCL Semantics in Isabelle/HOL / |r Achim D. Brucker and Burkhart Wolff -- |t Explicit Universes for the Calculus of Constructions / |r Judicael Courant -- |t Formalised Cut Admissibility for Display Logic / |r Jeremy E. Dawson and Rajeev Gore -- |t Formalizing the Trading Theorem for the Classification of Surfaces / |r Christophe Dehlinger and Jean-Francois Dufourd -- |t Free-Style Theorem Proving / |r David Delahaye -- |t A Comparison of Two Proof Critics: Power vs. Robustness / |r Louise A. Dennis and Alan Bundy -- |t Two-Level Meta-reasoning in Coq / |r Amy P. Felty -- |t PuzzleTool: An Example of Programming Computation and Deduction / |r Michael J. C. Gordon -- |t A Formal Approach to Probabilistic Termination / |r Joe Hurd -- |t Using Theorem Proving for Numerical Analysis / |r Micaela Mayero -- |t Quotient Types: A Modular Approach / |r Aleksey Nogin -- |t Sequent Schema for Derived Rules / |r Aleksey Nogin and Jason Hickey -- |t Algebraic Structures and Dependent Records / |r Virgile Prevosto, Domien Doligez and Therese Hardin -- |t Proving the Equivalence of Microstep and Macrostep Semantics / |r Klaus Schneider -- |t Weakest Precondition for General Recursive Programs Formalized in Coq / |r Xingyuan Zhang, Malcolm Munro, Mark Harman and Lin Hu |
| 520 | |a This book constitutes the refereed proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2002, held in Hampton, VA, USA in August 2002. The 20 revised full papers presented together with 2 invited contributions were carefully reviewed and selected from 34 submissions. All current issues in HOL theorem proving and formal verification of software and hardware systems are addressed. Among the HOL theorem proving systems evaluated are Isabelle/HOL, Isabelle/Isar, and Coq | ||
| 530 | |a Also available online via the World Wide Web; access restricted to licensed sites/users | ||
| 530 | |a Also available via the World Wide Web | ||
| 546 | |a English | ||
| 650 | 0 | |a Automatic theorem proving |v Congresses | |
| 650 | 6 | |a Théorèmes |x Démonstration automatique |v Congrès | |
| 650 | 7 | |a Automatic theorem proving |2 fast | |
| 655 | 7 | |a Actes de congrès |2 rvmgf | |
| 655 | 7 | |a Conference papers and proceedings |2 fast | |
| 655 | 7 | |a Conference papers and proceedings |2 lcgft | |
| 655 | 7 | |a proceedings (reports) |2 aat | |
| 700 | 1 | |a Carreño, Victor A., |d 1956- |1 https://id.oclc.org/worldcat/entity/E39PBJrRdGf8R7H9TWW6BWHBfq | |
| 700 | 1 | |a Carreño, Victor A., |d 1956- | |
| 700 | 1 | |a Muñoz, César A., |d 1968- |1 https://id.oclc.org/worldcat/entity/E39PCjvwFtVD8YhMVB9r4dPKMP | |
| 700 | 1 | |a Muñoz, César A., |d 1968- | |
| 700 | 1 | |a Tahar, Sofiène, |d 1966- |1 https://id.oclc.org/worldcat/entity/E39PCjHgc7KXJggKyjvrjmvrFX | |
| 700 | 1 | |a Tahar, Sofiène, |d 1966- | |
| 776 | 0 | 8 | |i Print version:TPHOLs 2002 (2002 : Hampton, Va.) |t Theorem proving in higher order logics : 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002 : proceedings |w (OCoLC)50252017 |
| 776 | 1 | |w (OCoLC)50393706 | |
| 830 | 0 | |a Lecture notes in computer science ; |v 2410 | |
| 830 | 0 | |a Lecture notes in computer science |p Lecture notes in artificial intelligence. | |
| 999 | 1 | 0 | |i e6334b4f-e7e4-4c80-83a5-e1caaacda7a3 |l in00000081690 |s US-CST |m theorem_proving_in_higher_order_logics15th_international_conference_tp_____2002_______sprina________________________________________tphols_____________________________e |
| 999 | 1 | 0 | |i e6334b4f-e7e4-4c80-83a5-e1caaacda7a3 |l 990011225670106761 |s US-MCM |m theorem_proving_in_higher_order_logics15th_international_conference_tp_____2002_______sprina________________________________________tphols_____________________________e |
| 999 | 1 | 0 | |i e6334b4f-e7e4-4c80-83a5-e1caaacda7a3 |l 990031274820108501 |s US-NCD |m theorem_proving_in_higher_order_logics15th_international_conference_tp_____2002_______sprina________________________________________tphols_____________________________e |
| 999 | 1 | 1 | |l in00000081690 |s ISIL:US-CST |t BKS |b 7ddf83d8-cdb9-4898-8349-83408531b713 |y 7ddf83d8-cdb9-4898-8349-83408531b713 |p UNLOANABLE |
| 999 | 1 | 1 | |l in00000081690 |s ISIL:US-CST |t BKS |a SUL-ELECTRONIC |p UNLOANABLE |
| 999 | 1 | 1 | |l 990011225670106761 |s ISIL:US-MCM |t BKS |a LSA OCC |b 39080016569714 |c QA76.9.A96.I577 2002 |d 0 |x BOOK |y 23466158740006761 |p UNLOANABLE |
| 999 | 1 | 1 | |l 990031274820108501 |s ISIL:US-NCD |t BKS |a LSC PSV |b D02407587X |c 001.64 L471, v. 2410 |d 1 |x BOOK |y 23718585640008501 |p LOANABLE |