Electronic Notes in Theoretical Computer Science, Volume 23

Volume 23, Number 1, 1999

• Lars Birkedal, Jaap van Oosten, Giuseppe Rosolini, Dana S. Scott:
  Preface.
  
• Samson Abramsky:
  Process Realizability.
  
• Sergei N. Artëmov:
  Uniform provability realization of intuitionistic logic, modality and lambda-terms.
  
• Steven Awodey, Lars Birkedal, Dana S. Scott:
  Local Realizability Toposes and a Modal Logic for Computability.
  
• Ulrich Berger:
  Effectivity and Density in Domains: A Survey.
  
• Lars Birkedal:
  Bibliography on Realizability.
  
• Tristan Crolard:
  A type theory which is complete for Kreisel's modified realizability.
  
• John Longley:
  Matching typed and untyped realizability.
  
• Jaap van Oosten:
  History and Developments.
  
• Andrew M. Pitts:
  Tripos Theory in Retrospect.
  
• Bernhard Reus:
  Realizability Models for Type Theories.
  
• Giuseppe Rosolini, Thomas Streicher:
  Comparing models of higher type computation.
  
• Martin Hyland:
  Variations on Realizability.
  

Volume 23, Number 2, 1999

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

Volume 23, Number 3, 1999

• Alessandro Armando, Tudor Jebelean:
  Preface.
  
• Fausto Giunchiglia:
  The OMRS project: State of the art.
  
• Alessandro Armando, Alessandro Coglio, Fausto Giunchiglia:
  The control component of open mechanized reasoning systems.
  
• Christoph Benzmüller, Mateja Jamnik, Manfred Kerber, Volker Sorge:
  Agent based mathematical reasoning.
  
• 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.
  
• Sylvain Boulmé, Thérèse Hardin, Daniel Hirschkoff, Valérie Ménissier-Morain, Renaud Rioboo:
  On the way to certify Computer Algebra Systems.
  
• Bruno Buchberger:
  Theory exploration versus theorem proving.
  
• Koji Nakagawa, Felix Kossak:
  User--system interaction within Theorema.
  
• Wolfgang Windsteiger:
  Building up hierarchical mathematical domains using functors in Theorema.
  
• Michael Beeson:
  Automatic derivation of the irrationality of e.
  
• Erica Melis, Volker Sorge:
  Employing external reasoners in proof planning.
  
• Andreas Franke, Michael Kohlhase:
  MBase: Representing mathematical knowledge in a relational data base.
  
• Olga Caprotti, Arjeh M. Cohen:
  Integrating computational and deduction systems using OpenMath.
  
• Alexander V. Lyaletski, Marina Morokovets:
  On linguistic aspects of integration of computer mathematical knowledge.