Type-theoretic languages: Proof search and semantics in conjunction with CADE-17, CMU Pittsburgh, PA, USA, June 20--21, 2000 (Q5926511)

The articles of this volume will be reviewed individually.NEWLINENEWLINEIndexed articles:NEWLINENEWLINE\textit{Hirokawa, Sachio; Nagano, Daisuke}, Long normal form proof search and counter-model generation, 11 p., electronic only [Zbl 0970.68143]NEWLINENEWLINE\textit{Harland, James A.; Pym, David J.; Winikoff, Michael}, Forward and backward chaining in linear logic. (Extended abstract), 16 p., electronic only [Zbl 0970.68028]NEWLINENEWLINE\textit{Nogin, Aleksey}, Writing constructive proofs yielding efficient extracted programs, 17 p., electronic only [Zbl 0970.68016]NEWLINENEWLINE\textit{Pym, David J.}, Notes towards a semantics for proof-search, 18 p. electronic only [Zbl 0970.68144]NEWLINENEWLINE\textit{Mylonakis, Nikos}, Proof assistance for refinement in type theory, 21 p., electronic only [Zbl 0970.68145]NEWLINENEWLINE\textit{Galmiche, D.; Notin, J. M.}, Proof-search and proof nets in mixed linear logic, 33 p., electronic only [Zbl 0971.68139]