Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings
type: Item
instance of: scholarly article
title: Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14--18, 2000. Proceedings
zbMATH Open document ID: 0944.00036
DOI: 10.1007/3-540-44659-1
published in: Lecture Notes in Computer Science
publication date: 2000-08-30T00:00:00Z
review text: 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ño, Víctor; Muñoz, César}, 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-o…
Mathematics Subject Classification ID: 00B25
Mathematics Subject Classification ID: 03-06
Mathematics Subject Classification ID: 68-06
zbMATH DE Number: 1498494
zbMATH Keywords: Portland, OR (USA)
zbMATH Keywords: Proceedings
zbMATH Keywords: Conference
zbMATH Keywords: TPHOLs 2000
zbMATH Keywords: Theorem proving
zbMATH Keywords: Higher order logics
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/3-540-44659-1
OpenAlex ID: W4298007499
description: scientific article; zbMATH DE number 1498494