Theoretical Computer Science, Volume 232

Volume 232, Numbers 1-2, 6 February 2000

• Didier Galmiche, David J. Pym:
  Proof-search in type-theoretic languages: an introduction. 5-53
  
• James L. Caldwell, Ian P. Gent, Judith L. Underwood:
  Search algorithms in type theory. 55-90
  
• Raymond McDowell, Dale Miller:
  Cut-elimination for a logic with definitions and induction. 91-119
  
• Toshiyasu Arai, Grigori Mints:
  Extended normal form theorems for logical proofs from axioms. 121-132
  
• Iliano Cervesato, Joshua S. Hodas, Frank Pfenning:
  Efficient resource management for linear logic proof search. 133-163
  
• Martin W. Bunder:
  Proof finding algorithms for implicational logics. 165-186
  
• Amy P. Felty:
  The calculus of constructions as a framework for proof search with set variable instantiation. 187-229
  
• Didier Galmiche:
  Connection methods in linear logic and proof nets construction. 231-272
  
• Gopalan Nadathur:
  Correspondences between classical, intuitionistic and uniform provability. 273-298
  
• Eike Ritter, David J. Pym, Lincoln A. Wallen:
  On the intuitionistic force of classical search. 299-333