FLoC'99 Second Federated Logic Conference

Volume 23, Number 1, 1999

A Tutorial Workshop on Realizability Semantics and Applications
A workshop associated to the 1999 Federated Logic Conference
Trento, Italy, June 30 - July 1, 1999

• 
  Samson Abramsky: Process Realizability. 1-2
• 
  Sergei N. Artëmov: Uniform provability realization of intuitionistic logic, modality and lambda-terms. 3-12
• 
  Steven Awodey, Lars Birkedal, Dana S. Scott: Local Realizability Toposes and a Modal Logic for Computability. 13-26
• 
  Ulrich Berger: Effectivity and Density in Domains: A Survey. 27-39
• 
  Lars Birkedal: Bibliography on Realizability. 40-57
• 
  Tristan Crolard: A type theory which is complete for Kreisel's modified realizability. 58-73
• 
  John Longley: Matching typed and untyped realizability. 74-100
• 
  Jaap van Oosten: History and Developments. 101-110
• 
  Andrew M. Pitts: Tripos Theory in Retrospect. 111-127
• 
  Bernhard Reus: Realizability Models for Type Theories. 128-158
• 
  Giuseppe Rosolini, Thomas Streicher: Comparing models of higher type computation. 159-165
• 
  Martin Hyland: Variations on Realizability: Simple examples realizing axioms of choice. 166-188
• 
  Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott: Preface. 189-190

Volume 23, Number 2, 1999

SMC'99 First International Workshop on Symbolic Model Checking
Trento, Italy, July 6, 1999

• 
  Felice Balarin: Concurrent Symbolic Verification of Liveness Properties for Interleaved Models. 1-10
• 
  Ranan Fraer, Gila Kamhi, Limor Fix, Moshe Y. Vardi: Evaluating Semi-Exhaustive Verification Techniques for Bug Hunting. 11-22
• 
  Shankar G. Govindaraju, David L. Dill: Approximate Symbolic Model Checking using Overlapping Projections. 23-33
• 
  Armin Biere, Edmund M. Clarke, Yunshan Zhu: Combining Local and Global Model Checking. 34-45
• 
  Fabio Somenzi: Symbolic State Exploration. 46-56
• 
  Sophie Renault, Eduard Cerny: Improving Termination of MDG-Based Abstract State Enumeration via Term Schematization. 57-74
• 
  Sérgio Vale Aguiar Campos, Marcio Teixeira, Marius Minea, Andreas Kuehlmann, Edmund M. Clarke: Model Checking Semi-Continuous Time Models Using BDDs. 75-87
• 
  Jesper B. Møller, Jakob Lichtenberg, Henrik Reif Andersen, Henrik Hulgaard: Fully Symbolic Model Checking of Timed Systems using Difference Decision Diagrams. 88-107
• 
  Laurent Ferier, Jean-François Raskin, Pierre-Yves Schobbens: Model-Generation of a Fictitious Clock Real-Time Logic Using Sharing Trees. 108-126
• 
  Alessandro Cimatti, Orna Grumberg: Preface. 127-128

Volume 23, Number 3, 1999

CALCULEMUS 99 Systems for Integrated Computation and Deduction
Trento, Italy, July 11-12, 1999

• 
  Alessandro Armando, Tudor Jebelean: Preface. 319-320
• 
  Fausto Giunchiglia: The OMRS project: State of the art. 321
• 
  Alessandro Armando, Alessandro Coglio, Fausto Giunchiglia: The control component of open mechanized reasoning systems. 322-339
• 
  Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge: Agent based mathematical reasoning. 340-351
• 
  Alexander A. Letichevsky, Julia V. Kapitonova, Vladislav A. Volkov, A. Chugayenko, Victor Khomenko, David R. Gilbert: The development of interactive algorithms for the Mathematical Environment. 352-369
• 
  Sylvain Boulmé, Thérèse Hardin, Daniel Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo: On the way to certify Computer Algebra Systems. 370-385
• 
  Bruno Buchberger: Theory exploration versus theorem proving. 386
• 
  Koji Nakagawa, Felix Kossak: User--system interaction within Theorema. 387-400
• 
  Wolfgang Windsteiger: Building up hierarchical mathematical domains using functors in Theorema. 401-419
• 
  Michael Beeson: Automatic derivation of the irrationality of e. 420-439
• 
  Erica Melis, Volker Sorge: Employing external reasoners in proof planning. 440-450
• 
  Andreas Franke, Michael Kohlhase: MBase: Representing mathematical knowledge in a relational data base. 451-468
• 
  Olga Caprotti, Arjeh M. Cohen: Integrating computational and deduction systems using OpenMath. 469-480
• 
  Alexander V. Lyaletski, Marina Morokovets: On linguistic aspects of integration of computer mathematical knowledge. 481-498