Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
type: Item
instance of: scholarly article
title: Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
zbMATH Open document ID: 0929.00038
DOI: 10.1007/3-540-48256-3
published in: Lecture Notes in Computer Science
publication date: 2000-01-06T00:00:00Z
review text: The articles of this volume will be reviewed individually. The preceding conference (11st, 1998) has been reviewed (see Zbl 0898.00030). Indexed articles: \textit{Völker, Norbert}, Disjoint sums over type classes in HOL, 5-18 [Zbl 0942.03013] \textit{Berghofer, Stefan; Wenzel, Markus}, Inductive datatypes in HOL -- lessons learned in formal-logic engineering, 19-36 [Zbl 0947.68128] \textit{Santen, Thomas}, Isomorphisms -- a link between the shallow and the deep, 37-54 [Zbl 0942.03011] \textit{Pfeifer, Holger; Rueß, Harald}, Polytypic proof construction, 55-72 [Zbl 0942.03012] \textit{Matthews, John}, Recursive function definition over coinductive types, 73-90 [Zbl 0944.03009] \textit{Capretta, Venanzio}, Universal algebra in type theory, 131-148 [Zbl 0947.08001] \textit{Zammit, Vincent}, On the implementation of an extensible declarative proof language, 185-202 [Zbl 0949.68139] \textit{Syme, Don}, Three tactic theorem proving, 203-220 [Zbl 0944.68162] \textit{Ambler, Simon J.; Crole, Roy L.}, Mechanized operational semantics via (co)induction, 221-238 [Zbl 0954.68093] \textit{Staples, Mark}, Representing WP semantics in Isabelle/ZF, 239-254 [Zbl 0944.68163] \textit{Schneider, Klaus; Hoffmann, Dirk W.}, A HOL conversion for translating linear time temporal logic to \(\omega\)-automata, 255-272 [Zbl 0943.03008] \textit{Grobauer, Bernd; Müller, Olaf}, From I/O automata to timed I/O automata. A solution to the ``Generalized Railroad Crossing'' in Isabelle/HOLCF, 273-289 [Zbl 0952.68128] \textit{Xiong, Haiyan; Curzon, Paul; Tahar, Sofiène}, Importing MDG verification results into HOL, 293-310 [Zbl 0969.94503]
Mathematics Subject Classification ID: 00B25
Mathematics Subject Classification ID: 03-06
Mathematics Subject Classification ID: 68-06
zbMATH DE Number: 1385385
zbMATH Keywords: Nice (France)
zbMATH Keywords: Proceedings
zbMATH Keywords: Conference
zbMATH Keywords: TPHOLs '99
zbMATH Keywords: Higher order logics
describes a project that uses: Isabelle/ZF
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/3-540-48256-3
OpenAlex ID: W4298072213
description: scientific article; zbMATH DE number 1385385