{"entities":{"Q701699":{"pageid":703548,"ns":120,"title":"Item:Q701699","lastrevid":42649150,"modified":"2025-07-07T16:37:56Z","type":"item","id":"Q701699","labels":{"en":{"language":"en","value":"Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20--23, 2002. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1825111"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701699$BCD1298A-0481-457C-AAD5-CFC15A7D85D5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cb101825dee41cb9a784b327413ed7203a81ff1e","datavalue":{"value":{"text":"Theorem proving in higher order logics. 15th international conference, TPHOLs 2002, Hampton, VA, USA, August 20--23, 2002. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q701699$1BF281A3-9F7A-4964-A91B-92FDBAD162DE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"beb21c5216c72edfb7e24a6535d6b9f7f8e9d872","datavalue":{"value":"0997.00025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$46540E9C-9BDB-4F0B-A5A3-C8FC5DF6F4C9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701699$E1E5E01F-A9F9-4AF1-8854-8C1E3C2A2620","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8fbcf3671e7e434b6806937c673340f2c084f23e","datavalue":{"value":{"time":"+2002-11-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q701699$7BC9D88A-99A9-45F0-A24F-CDC8B2EE9124","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"bb4860bc07706d04058e06300bbe4ed1eb52e307","datavalue":{"value":"The articles of mathematical interest will be reviewed individually. The preceding conference (14th, 2001) has been reviewed (see Zbl 0971.00027).  Indexed articles:  \\textit{Butler, Ricky}, Formal methods at NASA Langley, 1-2 [Zbl 1013.68735]  \\textit{Huet, G\u00e9rard}, Higher order unification 30 years later (Extended abstract), 3-12 [Zbl 1013.68541]  \\textit{Ambler, Simon J.; Crole, Roy L.; Momigliano, Alberto}, Combining higher order abstract syntax with tactical theorem proving and (co)induction, 13-30 [Zbl 1013.68545]  \\textit{Barthe, Gilles; Courtieu, Pierre}, Efficient reasoning about executable specifications in Coq, 31-46 [Zbl 1013.68539]  \\textit{Basin, David; Friedrich, Stefan; Gawkowski, Marek}, Verified bytecode model checkers, 47-66 [Zbl 1013.68544]  \\textit{Bauer, Gertrud; Nipkow, Tobias}, The 5 colour theorem in Isabelle/Isar, 67-82 [Zbl 1013.68200]  \\textit{Bertot, Yves; Capretta, Venanzio; Barman, Kuntal Das}, Type-theoretic functional semantics, 83-98 [Zbl 1013.68114]  \\textit{Brucker, Achim D.; Wolff, Burkhart}, A proposal for a formal OCL semantics in Isabelle/HOL, 99-114 [Zbl 1013.68538]  \\textit{Courant, Judica\u00ebl}, Explicit universes for the calculus of constructions, 115-130 [Zbl 1013.68540]  \\textit{Dawson, Jeremy E.; Gor\u00e9, Rajeev}, Formalised cut admissibility for display logic, 131-147 [Zbl 1013.03011]  \\textit{Dehlinger, Christophe; Dufourd, Jean-Fran\u00e7ois}, Formalizing the trading theorem for the classification of surfaces, 148-163 [Zbl 1013.68195]  \\textit{Delahaye, David}, Free-style theorem proving, 164-181 [Zbl 1013.68196]  \\textit{Dennis, Louise A.; Bundy, Alan}, A comparison of two proof critics: Power vs. robustness, 182-197 [Zbl 1013.68537]  \\textit{Felty, Amy P.}, Two-level meta-reasoning in Coq, 198-213 [Zbl 1013.68201]  \\textit{Gordon, Michael J. C.}, PuzzleTool: An example of programming computation and deduction, 214-229 [Zbl 1013.68542]  \\textit{Hurd, Joe}, A formal approach to probabilistic termination, 230-245 [Zbl 1013.68193]  \\textit{Mayero, Micaela}, Using theorem proving for numerical analysis. Correctness proof of an automatic differentiation algorithm, 246-262 [Zbl 1013.68203]  \\textit{Nogin, Aleksey}, Quotient types: A modular approach, 263-280 [Zbl 1013.68198]  \\textit{Nogin, Aleksey; Hickey, Jason}, Sequent schema for derived rules, 281-297 [Zbl 1013.68199]  \\textit{Prevosto, Virgile; Doligez, Damien; Hardin, Th\u00e9r\u00e8se}, Algebraic structures and dependent records, 298-313 [Zbl 1013.68194]  \\textit{Schneider, Klaus}, Proving the equivalence of microstep and macrostep semantics, 314-331 [Zbl 1013.68197]  \\textit{Zhang, Xingyuan; Munro, Malcolm; Harman, Mark; Hu, Lin}, Weakest precondition for general recursive programs formalized in Coq, 332-347 [Zbl 1013.68202]","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$D6391805-395A-466A-B2AB-3C0B56C311C8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$30F73FF9-D473-4F84-9078-23B0D6FDB4DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$0EEF41D1-3852-4C47-8A16-B0F2ADFC15FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$D47C4389-5B7B-426B-8FE1-9F08D3705C55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$4A3FC4B7-CDE9-4FC6-BD9B-E40FC1B58880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$49E10E11-492C-4572-84E7-123BB173214A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"723ad9946646c8490909c43ae7d9db3aa574b845","datavalue":{"value":"1825111","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q701699$39B0AA23-DF44-4EC5-9751-F86A37F60441","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9c4776bbce0df611ec8cfa0d7f53fa90f6318628","datavalue":{"value":"Hampton, VA (USA)","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$FD45E6D9-DEDE-430B-8661-DBE1FD543EB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$7B54275A-A244-4476-A72B-30CE8DCB9312","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d83ae477e518ffecea78688f13a2aaaeca13299","datavalue":{"value":"Conference","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$76FF1398-E3F7-4FDE-93BD-88C30F004645","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dde74a3c93bc0f803fbff7fbff0cc637d531336a","datavalue":{"value":"TPHOLs 2002","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$DA0868A7-FFD5-4281-B9EF-4A395237EA9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"742acadec2058a1daf33969cf122f1e00d23a668","datavalue":{"value":"Theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$C8068C6B-12C2-4DF4-AF08-8F9F93724E15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9cb067f7b7fd6a412bdd4ccb326a4a1cda3e4688","datavalue":{"value":"Higher order logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q701699$BCBA38E9-F74B-46A5-94BD-1593ABDCC30A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701699$D590F8DA-3AAD-4D42-8DC6-616D06125302","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q701699$725FC059-E77D-4068-B5FC-1C6B85BBDC2C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:701699","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:701699"}}}}}