{"entities":{"Q1578436":{"pageid":1589176,"ns":120,"title":"Item:Q1578436","lastrevid":72236517,"modified":"2026-04-14T03:32:12Z","type":"item","id":"Q1578436","labels":{"en":{"language":"en","value":"Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1498494"}},"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":"Q1578436$B4DE6EAD-6024-4A21-A5A0-1C063E876C21","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9c4a38a9e5eafe2654e72fd4523c2c3120cd7ad8","datavalue":{"value":{"text":"Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1578436$1F27FEA5-9CC0-4945-8953-A88B44B7A68E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4f8bf923bb8c7dbbfd9ff7bf3ab7f037ec07890d","datavalue":{"value":"0944.00036","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$025CC14D-1E31-4BF7-879A-8FA64FDC7B71","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d8de8e517698c899ec4260e70efc381c3bf29877","datavalue":{"value":"10.1007/3-540-44659-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$A86DFE48-0642-4D48-B98B-3B9AAB287199","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":"Q1578436$C025BA3A-8BE8-4017-B448-323C283A437E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6586588445949d2fbb40c4309ca2cd89ad6a7878","datavalue":{"value":{"time":"+2000-08-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1578436$2D100D25-9347-454F-A67D-5CD26388266D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"83424de0022f899302a02c6df4d7124198679ca2","datavalue":{"value":"The articles of mathematical interest will be reviewed individually. The preceding conference (12th, 1999) has been reviewed (see Zbl 0929.00038).  Indexed articles:  \\textit{Balaa, Antonia; Bertot, Yves}, Fix-point equations for well-founded recursion in type theory, 1-16 [Zbl 0974.68183]  \\textit{Barras, Bruno}, Programming and computing in HOL, 17-37 [Zbl 0974.68187]  \\textit{Berghofer, Stefan; Nipkow, Tobias}, Proof terms for simply typed higher order logic, 38-52 [Zbl 0974.03013]  \\textit{Bhargavan, Karthikeyan; Gunter, Carl A.; Obradovic, Davor}, Routing information protocol in HOL/SPIN, 53-72 [Zbl 0974.68010]  \\textit{Capretta, Venanzio}, Recursive families of inductive types, 73-89 [Zbl 0974.03014]  \\textit{Carre\u00f1o, V\u00edctor; Mu\u00f1oz, C\u00e9sar}, Aircraft trajectory modeling and alerting algorithm verification, 90-105 [Zbl 0974.68548]  \\textit{Colwell, Bob; Brennan, Bob}, Intel's formal verification experience on the Willamette development, 106-107 [Zbl 0974.68558]  \\textit{Denney, Ewen}, A prototype proof translator from HOL to Coq, 108-125 [Zbl 0974.68533]  \\textit{Dubois, Catherine}, Proving ML type soundness within Coq, 126-144 [Zbl 0974.68188]  \\textit{Fleuriot, Jacques D.}, On the mechanization of real analysis in Isabelle/HOL, 145-161 [Zbl 0974.68186]  \\textit{Geuvers, H.; Wiedijk, F.; Zwanenburg, J.}, Equational reasoning via partial reflection, 162-178 [Zbl 0974.68182]  \\textit{Gordon, Michael J. C.}, Reachability programming in HOL98 using BDDs, 179-196 [Zbl 0974.68189]  \\textit{Gottliebsen, Hanne}, Transcendental functions and continuity checking in PVS, 197-214 [Zbl 0974.68190]  \\textit{Grundy, Jim}, Verified optimization for the Intel IA-64 architecture, 215-232 [Zbl 0974.68567]  \\textit{Harrison, John}, Formal verification of IA-64 division algorithms, 233-251 [Zbl 0974.68535]  \\textit{Hickey, Jason; Nogin, Aleksey}, Fast tactic-based theorem proving, 252-267 [Zbl 0974.68534]  \\textit{Hofmann, Martin; Tang, Francis}, Implementing a program logic of objects in a higher-order logic theorem prover, 268-282 [Zbl 0974.68185]  \\textit{Holmes, M. Randall}, A strong and mechanizable grand logic, 283-300 [Zbl 0974.03012]  \\textit{Huisman, Marieke; Jacobs, Bart}, Inheritance in higher order logic: Modeling and reasoning, 301-319 [Zbl 0974.68033]  \\textit{Jackson, Paul B.}, Total-correctness refinement for sequential reactive systems, 320-337 [Zbl 0974.68119]  \\textit{Kaivola, Roope; Aagaard, Mark D.}, Divider circuit verification with model checking and theorem proving, 338-355 [Zbl 0974.68519]  \\textit{Kerb\u0153uf, Micka\u00ebl; Nowak, David; Talpin, Jean-Pierre}, Specification and verification of a steam-boiler with Signal-Coq, 356-371 [Zbl 0974.68522]  \\textit{Laibinis, Linas; von Wright, Joakim}, Functional procedures in higher-order logic, 372-387 [Zbl 0974.68506]  \\textit{Letouzey, Pierre; Th\u00e9ry, Laurent}, Formalizing St\u00e5lmarck's algorithm in Coq, 388-405 [Zbl 0974.68184]  \\textit{L\u00fcth, Christoph; Wolff, Burkhart}, TAS -- a generic window inference system, 406-423 [Zbl 0974.68507]  \\textit{Merz, Stephan}, Weak alternating automata in Isabelle/HOL, 424-441 [Zbl 0974.68090]  \\textit{Milner, Robin}, Graphical theories of interactive systems: Can a proof assistant help?, 442 [Zbl 0974.68555]  \\textit{Mokkedem, Abdel; Leonard, Tim}, Formal verification of the Alpha 21364 network protocol, 443-461 [Zbl 0974.68553]  \\textit{Pollack, Robert}, Dependently typed records for representing mathematical structure, 462-479 [Zbl 0974.68181]  \\textit{Reus, Bernhard; Hein, Tatjana}, Towards a machine-checked Java specification book, 480-497 [Zbl 0974.68505]  \\textit{Slind, Konrad}, Another look at nested recursion, 498-518 [Zbl 0974.68180]  \\textit{Wos, Larry; Fitelson, Branden}, Automating the search for answers to open questions, 519-525 [Zbl 0974.68538]  \\textit{Wos, Larry}, Appendix: conjectures concerning proof, design, and verification, 526-533 [Zbl 0974.68537]","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$D5365467-8B37-444B-A459-A3D4325FDA42","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6f2c17db95e93f9a5a19ff6c68b3a1df8b0c021e","datavalue":{"value":"00B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$0861978A-B49E-4169-8126-F1B230B60CE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f1971b12f93143b2604d15a1750f495d71fae62d","datavalue":{"value":"03-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$A524583C-E5CC-412A-9A4B-DFB8F08E13B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ed293b811733fa9438a72e1b6ba5680a0d2aac9e","datavalue":{"value":"68-06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$C18738B4-56BB-40BF-AEC5-D3B9D176A57A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4e057f18f684d7b841d362beb02d95a22196a0bf","datavalue":{"value":"1498494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$AC087811-A32D-43BD-8208-A57B7FFB5562","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7490cb00cb00b00dad90b3e67628a99ca9fa9e9c","datavalue":{"value":"Portland, OR (USA)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$7C99C7DB-7C3F-4A52-BF94-4F1E6A96D071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5c4c4bb5a86a0fdf66f908b603f2f6975f5ef6fc","datavalue":{"value":"Proceedings","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$75E93E1E-CBC2-4F2E-94F8-369B24AEC629","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d83ae477e518ffecea78688f13a2aaaeca13299","datavalue":{"value":"Conference","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$8039DD01-4A9F-422B-83ED-A63EF1832F81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"288e55e993a88e92332232ecbe9b940221d71cf4","datavalue":{"value":"TPHOLs 2000","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$6DF4AB21-2DAA-4769-83F8-22CD61395239","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"742acadec2058a1daf33969cf122f1e00d23a668","datavalue":{"value":"Theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$41EBA236-600D-496F-A423-188AA443D1F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9cb067f7b7fd6a412bdd4ccb326a4a1cda3e4688","datavalue":{"value":"Higher order logics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1578436$CBC011E8-2A5F-41C5-9EC8-36C4D30A8A2A","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":"Q1578436$4EC4088F-FDBE-4677-819D-5016826A4220","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1578436$CB1200AC-EE79-47F4-8AFA-E6E9859033D6","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":"Q1578436$4EAFC8DF-C56D-4C54-9D6A-26CFA1BA9C9D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a378e1e394015de7399f3e96c2d16d93f72a85fb","datavalue":{"value":"https://doi.org/10.1007/3-540-44659-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q1578436$2548F3D2-2151-4AC8-BC40-741B61D34699","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b08b679bacc73e71ea941366fa0e90ac755b2485","datavalue":{"value":"W4298007499","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1578436$3E4088FC-73F6-4F89-B754-CE89D528E2D7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Theorem_proving_in_higher_order_logics._13th_international_conference,_TPHOLs_2000,_Portland,_OR,_USA,_August_14--18,_2000._Proceedings"}}}}}