@article{Galmiche-Pym/00,
AUTHOR = {Galmiche, Didier and Pym, David J.},
TITLE = {Proof-search in type-theoretic languages: An introduction},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {5-53},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Caldwell-Gent-Underwood/00,
AUTHOR = {Caldwell, James L. and Gent, Ian P. and Underwood, Judith},
TITLE = {Search algorithms in type theory},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {55-90},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{McDowell-Miller/00,
AUTHOR = {McDowell, Raymond and Miller, Dale},
TITLE = {Cut-elimination for a logic with definitions and induction},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {91-119},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Arai-Mints/00,
AUTHOR = {Arai, Toshiyasu and Mints, Grigori},
TITLE = {Extended normal form theorems for logical proofs from axioms},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {121-132},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Cervesato-Hodas-Pfenning/00,
AUTHOR = {Cervesato, Iliano and Hodas, Joshua S. and Pfenning, Frank},
TITLE = {Efficient resource management for linear logic proof search},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {133-163},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Bunder/00,
AUTHOR = {Bunder, M.W.},
TITLE = {Proof finding algorithms for implicational logics},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {165-186},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Felty/00,
AUTHOR = {Felty, Amy},
TITLE = {The calculus of constructions as a framework for proof search with set variable instantiation},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {187-229},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Galmiche/00,
AUTHOR = {Galmiche, D.},
TITLE = {Connection methods in linear logic and proof nets construction},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {231-272},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Nadathur/00,
AUTHOR = {Nadathur, Gopalan},
TITLE = {Correspondences between classical, intuitionistic and uniform provability},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {273-298},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}
@article{Ritter-Pym-Wallen/00,
AUTHOR = {Ritter, Eike and Pym, David and Wallen, Lincoln},
TITLE = {On the intuitionistic force of classical search},
JOURNAL = {Theor.~Comput.~Sci.},
VOLUME = {232},
NUMBER = {1-2},
PAGES = {299-333},
YEAR = {2000},
PUBLISHER = {Elsevier Science Publishers B.V. (North Holland)},
ADDRESS = {Amsterdam-Lausanne-New York-Oxford-Shannon-Tokyo},
}