%A R. Milner
%T Some uses of maximal fixed points (abstract)
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 3-6

%A V. Breazu-Tannen
%A A. Meyer
%T Polymorphism is conservative over simple types
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 7-17

%A J. Goguen
%A J. Messeguer
%T Order-sorted algebra solves the constructor-selector problem
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 18-29

%A N. Mendler
%T Recursive types and type constraints in second-order lambda calculus
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 30-36

%A M. Wand
%T Complete type inference for simple objects
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 37-46

%A S. Abramsky
%T Domain theory in logical form
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 47-53

%A D. Harel
%A A. Pnueli
%A J. Schmidt
%A R. Sherman
%T On the formal semantics of statecharts
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 54-64

%A R. Seely
%T Modeling computations: a 2-categorical framework
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 65-71

%A H. Gaifman
%A V. Pratt
%T Partial order models of concurrency and the computation of functions
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 72-88

%A N. Bidoit
%A C. Froidevaux
%T Minimalism subsumes default logic and circumscription
in stratified logic programming
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 89-97

%A D. Miller
%A G. Nadathur
%A A. Scedrov
%T Hereditary Harrop formulas and uniform proof systems
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 98-105

%A H. Gaifman
%A H. Mairson
%A Y. Sagiv
%A M. Vardi
%T Undecidable optimization problems for database logic programs
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 106-118

%A J. Reynolds
%T Conjunctive types and Algol-like languages (abstract)
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 119-122

%A M. Abadi
%T The power of temporal proofs
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 123-130

%A B. Alpern
%A F. Schneider
%T Proving boolean combinations of deterministic properties
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 131-137

%A A. Sistla
%A S. German
%T Reasoning with many processes
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 138-152

%A A. Sistla
%A L. Zuck
%T On the eventuality operator in temporal logic
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 153-166

%A M. Vardi
%T Verification of concurrent programs: the automata-theoretic framework
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 167-178

%A M.H. van\ Emden
%T First-order predicate logic
as a common basis for relational and functional programming (abstract)
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 179-182

%A R. Constable
%A S. Smith
%T Partial objects in constructive type theory
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 183-193

%A R. Harper
%A F. Honsell
%A G. Plotkin
%T A framework for defining logics
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 194-204

%A D. Howe
%T The computational behaviour of Girard's paradox
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 205-214

%A S. Allen
%T A non-type-theoretic definition of Martin-lof's types
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 215-224

%A A. Kfoury
%A J. Tiuryn
%A P. Urzyczyn
%T The hierarchy of finitely typed functional programs
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 225-235

%A N. Immerman
%A D. Kozen
%T Definability with bounded number of bound variables
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 236-244

%A W. Thomas
%T On chain logic, path logic, and first-order logic over infinite trees
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 245-256

%A J. Halpern
%A E. Wimmers
%T Full abstraction and expressive completeness for FP
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 257-274

%A Y. Shoham
%T A semantical approach to nonmonotonic logics
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 275-279

%A R. Faigin
%A J. Halpern
%T I'm OK if you're OK: on the notion of trusting communication
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 280-292

%A A. Goerdt
%T Hoare logic for lambda-terms as basis of Hoare logic for imperative languages
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 293-302

%A J. Mitchell
%A E. Moggi
%T Kripke-style models for typed lambda calculus
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 303-314

%A P. Freyd
%A A. Scedrov
%T Some semantic aspects of polymorphic lambda calculus
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 315-319

%A C. Bohm
%A E. Tronci
%T X-separability and left-invertibility in x-calculus
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 320-330

%A L. Bachmair
%T Inference rules for rewrite-based first-order theorem proving
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 331-337

%A J. Gallier
%A S. Raatz
%A W. Snyder
%T Theorem proving using rigid E-unification: equational matings
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 338-346

%A C. Kirchner
%A P. Lescanne
%T Solving disequations
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 347-352

%A M. Dauchet
%A T. Heuillard
%A P. Lescanne
%A S. Tison
%T Decidability of the confluence of ground term rewriting systems
%J Proceedings of the Second Annual Conference on Logics in Computer Science
%C Ithaca, New York
%D June 1987
%K lics lics2
%P 353-360