%%% ====================================================================
%%%  BibTeX-file{
%%%     author          = "David M. Jones",
%%%     version         = "2.03",
%%%     date            = "14 July 1992",
%%%     time            = "14:48:25 EDT",
%%%     filename        = "lics.bib",
%%%     address         = "MIT Laboratory for Computer Science
%%%                        Room NE43-316
%%%                        545 Technology Square
%%%                        Cambridge, MA 02139
%%%                        USA",
%%%     telephone       = "(617) 253-5936",
%%%     FAX             = "(617) 253-3480",
%%%     checksum        = "39895 3855 18362 145591",
%%%     email           = "dmjones at theory.lcs.mit.edu",
%%%     codetable       = "ISO/ASCII",
%%%     keywords        = "LICS, logic, bibliography, BibTeX",
%%%     supported       = "yes",
%%%     docstring       = "The checksum field above contains a CRC-16
%%%                        checksum as the first value, followed by the
%%%                        equivalent of the standard UNIX wc (word
%%%                        count) utility output of lines, words, and
%%%                        characters.  This is produced by Robert
%%%                        Solovay's checksum utility.",
%%%  }
%%% ====================================================================

                       Annual IEEE Symposium on
                      LOGIC IN COMPUTER SCIENCE

This is a BibTeX database for papers appearing in the proceedings of
the annual IEEE Symposium on Logic in Computer Science.  See the end
of the file for cross reference entries.

Entries are organized by the year in which they appeared and, within
each year, by the order in which they appeared in the proceedings.

Abstracts are currently given for only about 35% of the papers.
Authors of papers whose abstracts are not included are encouraged to
send their abstracts to dmjones at theory.lcs.mit.edu.  Corrections to
the bibliography should be sent to the same address.  Authors are also
encouraged to send information about publication of extended versions
of LICS papers.

For documentation on using this file, see Section 4.3 and Appendix B
of "LaTeX: A Document Preparation System" by Leslie Lamport.  For
information on the crossref feature, see the article "BibTeXing" by
Oren Patashnik (8 Feburary 1988), which is distributed with the BibTeX
0.99b source code.

For information on ordering backissues, write to

    IEEE Computer Society Press         IEEE Service Center
    Customer Service Center             445 Hoes Lange
    10662 Los Vaqueros Circle           PO Box 1331
    PO Box 3014                         Piscataway, NJ 08855-1331
    Los Alamitos, CA 90720-1264

    IEEE Computer Society               IEEE Computer Society
    13, avenue de l'Aquilon             Ooshima Building
    B-1200 Brussels                     2-19-1 Minami-Aoyama
    BELGIUM                             Minato-ku, Tokyo 107
                                        JAPAN


			       1st LICS
                           June 16-18, 1986
                       Cambridge, Massachusetts

@InProceedings{Robinson86,
author={J. A. Robinson},
title={Merging Functional with Relational Programming in a Reduction
Setting (Abstract of an Invited Lecture)},
pages={2},
crossref={LICS1}
}

@InProceedings{Csirmaz86,
author={Laszlo Csirmaz and Bradd Hart},
title={Program Correctness on Finite Fields},
pages={4--10},
crossref={LICS1}
}

@InProceedings{GermanCH86,
author={Steven M. German and Edmund M. Clarke and  Joseph Y. Halpern},
title={True Relative Completeness of an Axiom System for the Language
{L4} (Abridged)},
pages={11--25},
crossref={LICS1}
}

@InProceedings{JonssonMW86,
author={Bengt Jonsson and Zohar Manna and Richard Waldinger},
title={Towards Deductive Synthesis of Dataflow Networks},
pages={26--37},
crossref={LICS1}
}

@InProceedings{RoundsK86,
author={William C. Rounds and Robert Kasper},
title={A Complete Logical Calculus for Record Structures Representing
Linguistic Information},
pages={38--43},
crossref={LICS1}
}

@InProceedings{Meyer87a,
author={Albert R. Meyer},
title={{F}loyd-{H}oare Logic Defines Semantics: Preliminary Version},
crossref={LICS1},
pages={44--48},
note={To appear in } # tcs,
abstract={The first-order partial correctness assertions provable in
Floyd-Hoare logic about an uninterpreted {\em while\/}-program scheme
determine the scheme up to equivalence.  This settles an open problem
of Meyer and Halpern~\cite{MeyerH82}.  The simple proof of this fact
carries over to other partial correctness axiomatizations given in the
literature for wider classes of {\sc Algol}-like program schemes.}
}

@InProceedings{BeckmanGW86,
author={Lennart Beckman and Rune Gustavsson and Annika W{\ae}rn},
title={An Algebraic Model of Parallel Execution of Logic Programs},
pages={50--57},
crossref={LICS1}
}

@InProceedings{Brookes86,
author={S. D. Brookes},
title={A Semantically Based Proof System for Partial Correctness and
Deadlock in {CSP}},
pages={58--65},
crossref={LICS1}
}

@InProceedings{MonteiroP86,
author={Lu{\'\i}s Monteiro and Fernando C. N. Pereira},
title={A Sheaf-Theoretic Model of Concurrency},
pages={66--76},
crossref={LICS1}
}

@InProceedings{BensonB86,
author={David B. Benson and Ofer Ben-Shachar},
title={Strong Bisimulation of State Automata},
pages={77--81},
crossref={LICS1}
}

@InProceedings{Mohring86,
author={Christine Mohring},
title={Algorithm Development in the Calculus of Constructions},
pages={84--91},
crossref={LICS1}
}

@InProceedings{Schlipf86,
author={John S. Schlipf},
title={How Uncomputable is General Circumscription? (Extended Abstract)},
pages={92--95},
crossref={LICS1}
}

@InProceedings{Shultis86,
author={J. Shultis},
title={The Design and Implementations of {Intuit}},
pages={96--104},
crossref={LICS1}
}

@InProceedings{Mason86,
author={Ian A. Mason},
title={Equivalence of First Order {LISP} Programs.  Proving Properties
of Destructive Programs via Transformation},
pages={105--117},
crossref={LICS1}
}

@InProceedings{AmadioBL86,
author={Roberto Amadio and Kim B. Bruce and Giuseppe Longo},
title={The Finitary Projection Model for Second Order Lambda Calculus
and Solutions to Higher Order Domain Equations},
pages={122--130},
crossref={LICS1}
}

@InProceedings{FelleisenFKD86,
author={Matthias Felleisen and Daniel P. Friedman and Eugene
Kohlbecker and Bruce Duba},
title={Reasoning with Continuations},
pages={131--141},
crossref={LICS1}
}

@InProceedings{Gunter86,
author={Carl A. Gunter},
title={The Largest First-Order-Axiomatizable {Cartesian} Closed
Category of Domains},
pages={142--148},
crossref={LICS1}
}

@InProceedings{HalpernWW86,
author={Joseph Y. Halpern and John H. Williams and Edward L. Wimmers},
title={Good Rewrite Strategies for {FP}},
pages={149--162},
crossref={LICS1}
}

@InProceedings{Plaisted86,
author={David A. Plaisted},
title={The Denotional Semantics of Nondeterministic Recursive Programs
using Coherent Relations},
pages={163--174},
crossref={LICS1}
}

@InProceedings{AbadiM86,
author={Mart{\'\i}n Abadi and Zohar Manna},
title={A Timely Resolution},
pages={176--186},
crossref={LICS1}
}

@InProceedings{ChouK86,
author={Shang-ching Chou and Hai-Ping Ko},
title={On Mechanical Theorem Proving in {Minkowskian} Plane Geometry},
pages={187--192},
crossref={LICS1}
}

@InProceedings{Despeyroux86,
author={Jo{\"e}lle Despeyroux},
title={Proof of Translation in Natural Semantics},
pages={193--205},
crossref={LICS1}
}

@InProceedings{Kirchner86,
author={Claude Kirchner},
title={Computing Unification Algorithms},
pages={206--216},
crossref={LICS1}
}

@InProceedings{CoppoZ86,
author={M. Coppo and M. Zacchi},
title={Type inference and logical relations},
pages={218--226},
crossref={LICS1}
}

@InProceedings{Coquand86,
author={Thierry Coquand},
title={An Analysis of {Girard's} Paradox},
pages={227--236},
crossref={LICS1}
}

@InProceedings{KnoblockC86,
author={Todd B. Knoblock and Robert L. Constable},
title={Formalized Metareasoning in Type Theory},
pages={237--248},
crossref={LICS1}
}

@InProceedings{MendlerPC86,
author={N. P. Mendler and P. Panangaden and R. L. Constable},
title={Infinite Objects in Type Theory},
pages={249--255},
crossref={LICS1}
}

@InProceedings{Girard86,
author={Jean-Yves Girard},
title={Quantitative and Qualitative Semantics (Abstract of Invited
Lecture)},
pages=258,
crossref={LICS1}
}

@InProceedings{Browne86,
author={Michael C. Browne},
title={An Improved Algorithm for the Automatic Verification of Finite
State Systems Using Temporal Logic},
pages={260--266},
crossref={LICS1}
}

@InProceedings{EmersonL86,
author={E. Allen Emerson and Chin-Laung Lei},
title={Efficient Model Checking in Fragments of the Propositional
Mu-Calculus (Extended Abstract)},
pages={267--278},
crossref={LICS1}
}

@InProceedings{HalpernS86,
author={Joseph Y. Halpern and Yoav Schoham},
title={A Propositional Model Logic of Time Intervals},
pages={279--292},
crossref={LICS1}
}

@InProceedings{MakowskyS86,
author={J. A. Makowsky and I. Sain},
title={On the Equivalence of Weak Second Order and Nonstandard Time
Semantics For Various Program Verification Systems},
pages={293--300},
crossref={LICS1}
}

@InProceedings{PerrinS86,
author={Dominique Perrin and Paul E. Schupp},
title={Automata on the Integers, Recurrence Distinguishability, and
the Equivalence and Decidability of Monadic Theories},
pages={301--304},
crossref={LICS1}
}

@InProceedings{RosnerP86,
author={Roni Rosner and Amir Pnueli},
title={A Choppy Logic},
pages={306--313},
crossref={LICS1}
}

@InProceedings{Parikh86,
author={Rohit Parikh},
title={Levels of Knowledge in Distributed Computing},
pages={314--321},
crossref={LICS1}
}

@InProceedings{PnueliZ86,
author={Amir Pnueli and Lenore Zuck},
title={Probabilistic Verification by Tableaux},
pages={322--331},
crossref={LICS1}
}

@InProceedings{VardiW86,
author={Moshe Y. Vardi and Pierre Wolper},
title={An Automata-Theoretic Approach to Automatic Program
Verification (Preliminary Report)},
pages={332--344},
crossref={LICS1}
}

@InProceedings{BachmairDH86,
author={Leo Bachmair and Nachum Dershowitz and Jieh Hsiang},
title={Orderings for Equational Proofs},
pages={346--357},
crossref={LICS1}
}

@InProceedings{JouannaudK86,
author={Jean-Pierre Jouannaud and Emmanuel Kounalis},
title={Automatic Proofs by Induction in Equational Theories Without
Constructors},
pages={358--366},
crossref={LICS1}
}

@InProceedings{KapurM86,
author={Deepak Kapur and David R. Musser},
title={Inductive Reasoning with Incomplete Specifications (Preliminary
Report)},
pages={367--377},
crossref={LICS1}
}

@InProceedings{Statman86,
author={Rick Statman},
title={On Translating Lambda Terms into Combinators; The Basis Problem},
pages={378--382},
crossref={LICS1}
}


			       2nd LICS
                           June 22-25, 1987
                           Ithaca, New York


@InProceedings{Milner87,
author={R. Milner},
title={Some Uses of Maximal Fixed Points (Abstract of Invited Lecture)},
pages={3},
crossref={LICS1},
abstract={The notions of indistinguishability and ``lack of
discrepancy'' are captured by maximal fixed points.  Results in
concurrent processes and operational semantics will be discussed.}
}

@InProceedings{Breazu-TannenM87,
author={Val Breazu-Tannen and Albert R. Meyer},
title={Polymorphism is conservative over simple types (Preliminary Report)},
pages={7--17},
crossref={LICS1},
abstract={The addition of the Girard-Reynolds polymorphic constructs
to arbitrary simply typed equational lambda theories is conservative.
This implies that polymorphism can be superimposed on familiar
programming languages without changing their behavior.
\par
Using a purely syntactic method, an effective proof of conservative
extension is given for a polymorphic equational logic which is
complete when all types are assumed nonempty.  When polymorphic types
may be empty, the stronger result is proved that any model of the
simply typed lambda calculus can be fully and faithfully embedded in a
model of the polymorphic lambda calculus.}
}

@InProceedings{GoguenM87,
author={Joseph A. Goguen and Jos{\'e} Meseguer},
title={Order-Sorted Algebra solves the Constructor-Selector, Multiple},
pages={18--29},
crossref={LICS1}
}

@InProceedings{Mendler87,
author={N. P. Mendler},
title={Recursive Types and Type Constraints in Second-Order Lambda
Calculus},
pages={30--36},
crossref={LICS2}
}

@InProceedings{Wand87,
author={Mitchell Wand},
title={Complete Type Inference for Simple Objects},
pages={37--44},
crossref={LICS2}
}

@InProceedings{Abramksy87,
author={Samson Abramsky},
title={Domain Theory in Logical Form},
pages={47--53},
crossref={LICS2}
}

@InProceedings{HarelPSS87,
author={D. Harel and A. Pnueli and J. P. Schmidt and R. Sherman},
title={On the Formal Semantics of Statecharts (Extended Abstract)},
pages={54--64},
crossref={LICS2}
}

@InProceedings{Seely87,
author={R. A. G. Seely},
title={Modelling Computations: A 2-Categorical Framework},
pages={65--71},
crossref={LICS2}
}

@InProceedings{GaifmanP87,
author={Haim Gaifman and Vaughan Pratt},
title={Partial Order Models of Concurrency and the Computation of
Functions},
pages={72--85},
crossref={LICS2}
}

@InProceedings{BidoitF87,
author={N. Bidoit and C. Froidevaux},
title={Minimalism subsumes Default Logic and Circumscription in
Stratified Logic Programming},
pages={89--97},
crossref={LICS2}
}

@InProceedings{MillerNS87,
author={Dale Miller and Gopalan Nadathur and Andre Scedrov},
title={Hereditary {Harrop} Formulas and Uniform Proof Systems},
pages={98--105},
crossref={LICS2}
}

@InProceedings{GaifmannM87,
author={Haim Gaifman and Harry Mairson},
title={Undecidable Optimization Problems for Database Logic Programs},
pages={106--115},
crossref={LICS2}
}

@InProceedings{Reynolds87,
author={J. Reynolds},
title={Conjunctive Types and {Algol}-like Languages},
pages={119},
crossref={LICS2},
abstract={The idea of conjunctive types, i.e., that an identifier or
phrase can simultaneously possess several types, originated in the
work of Coppo and Dezani, who devised a conjunctive-type discipline
for the un-typed lambda calculus.  They showed that this discipline
provides a model of the language and, as a corollary, that there is no
algorithm for type inference.
\par
This results seems to have discouraged the use of conjunctive types in
practical programming languages; yet, is is not barrier to their use
in explicitly types languages.  We will explore the application of
conjunctive types to Algol-like languages and demonstrate that they
can make such languages both simpler and more flexible.}
}

@InProceedings{Abadi87,
author={Mart{\'\i}n Abadi},
title={The Power of Temporal Proofs},
pages={123--130},
crossref={LICS2}
}

@InProceedings{AlpernS87,
author={Bowen Alpern and Fred B. Schneider},
title={Proving {Boolean} Combinations of Deterministic Properties},
pages={131--137},
crossref={LICS2}
}

@InProceedings{SistlaG87,
author={A. P. Sistla and S. M. German},
title={Reasoning with Many Processes},
pages={138--152},
crossref={LICS2}
}

@InProceedings{SistlaZ87,
author={A. Prasad Sistla and Lenore D. Zuck},
title={On the Eventuality Operator in Temporal Logic},
pages={153--166},
crossref={LICS2}
}

@InProceedings{Vardi87,
author={Moshe Y. Vardi},
title={Verification of Concurrent Programs: The Automata-Theoretic
Framework},
pages={167--176},
crossref={LICS2}
}

@InProceedings{Emden87,
author={W. H. van Emdem},
title={First-order Predicate Logic as a Common Basis for Relational
and Functional Programming},
pages={179},
crossref={LICS2}
}

@InProceedings{ConstableS87,
author={Robert L. Constable and Scott Fraser Smith},
title={Partial Objects In Constructive Type Theory},
pages={183--193},
crossref={LICS2}
}

@InProceedings{HarperHP87,
author={Robert Harper and Furio Honsell and Gordon Plotkin},
title={A Framework for Defining Logics},
pages={194--204},
crossref={LICS2}
}

@InProceedings{Howe87,
author={Douglas J. Howe},
title={The Computational Behaviour of {Girard's} Paradox},
pages={205--214},
crossref={LICS2}
}

@InProceedings{Allen87,
author={Stuart Allen},
title={A Non-Type-Theoretic Definition of {Martin-L{\"o}f's} Types},
pages={215--221},
crossref={LICS2}
}

@InProceedings{KfouryTU87,
author={A. J. Kfoury and J. Tiuryn and P. Urzyczyn},
title={The Hierarchy of Finitely Typed Functional Programs (Short
Version)},
pages={225--235},
crossref={LICS2}
}

@InProceedings{ImmermanK87,
author={Neil Immerman and Dexter Kozen},
title={Definability with Bounded Number of Bound Variables},
pages={236--244},
crossref={LICS2}
}

@InProceedings{Thomas87,
author={Wolfgang Thomas},
title={On Chain Logic, Path Logic, and First-Order Logic over Infinite
Trees},
pages={245--256},
crossref={LICS2}
}

@InProceedings{HalpernW87,
author={Joseph Y. Halpern and Edward L. Wimmers},
title={Full Abstraction and Expressive Completenes for {FP}},
pages={257--271},
crossref={LICS2}
}

@InProceedings{Shoham87,
author={Yoav Shoham},
title={A Semantical Approach to Nonmonotic Logics},
pages={275--279},
crossref={LICS2}
}

@InProceedings{FaginH87,
author={Ronald Fagin and Joseph Y. Halpern},
title={I'm {OK} if You're {OK}: On the Notion of Trusting
Communication},
pages={280--292},
crossref={LICS2}
}

@InProceedings{Goerdt87,
author={Andreas Goerdt},
title={{H}oare Logic for Lambda-Terms as Basis of {H}oare Logic for
Imperative Languages},
pages={293--299},
crossref={LICS2}
}

@InProceedings{MitchellM87,
author={John C. Mitchell and Eugenio Moggi},
title={Kripke-Style models for typed lambda calculus},
pages={303--314},
crossref={LICS2}
}

@InProceedings{FreydS87,
author={Peter Freyd and Andre Scedrov},
title={Some Semantic Aspects of Polymorphic Lambda Calculus},
pages={315--319},
crossref={LICS2}
}

@InProceedings{BohmT87,
author={C. B{\"o}hm and E. Tronci},
title={X-Separability and Left-Invertibility in $\lambda$-calculus},
pages={320--328},
crossref={LICS2}
}

@InProceedings{BachmairD87,
author={Leo Bachmair and Nachum Dershowitz},
title={Inference Rules for Rewrite-Based First-Order Theorem Proving},
pages={331--337},
crossref={LICS2}
}

@InProceedings{GallierRS87,
author={Jean H. Gallier and Stan Raatz and Wayne Snyder},
title={Theorem Proving Using Rigid {$E$}-Unification Equational Matings},
pages={338--346},
crossref={LICS2}
}

@InProceedings{KirchnerL87,
author={Claude Kirchner and Pierre Lescanne},
title={Solving Disequations},
pages={347--352},
crossref={LICS2},
abstract={We present a general study of equations (objects of form $s
= t$) and disequations (objects of form $s = t$) solving. The problem
is approached from its fully general mathematical definition clearly
separating universally and existentially quantified variables. In
addition it is showed to have many connections with unification in
equational theories like associativity commutativity, in particular
methods similar to those used to solve equational unification problem
works in solving disequations.  This abstract framework is then
applied to study the sufficient completeness of a rewrite rule based
definition of a function.},
comment={Most of the results of this paper were also published in
``Equational Problems and Disunification,'' {\em Journal of Symbolic
Computation}, 7(3/4):371--426, March/April 1989.}
}

@InProceedings{DauchetTHL87,
author={Max Dauchet and Sophie Tison and Thierry Heuillard and Pierre
Lescanne},
title={Decidability of the Confluence of Ground Term Rewriting Systems},
pages={353-359},
crossref={LICS2},
abstract={The aim of this paper is to propose an algorithm to dedide
the confluence of finite ground term rewrite systems.  It is well
known that the confluence is not decidable for general term rewrite
systems, but this paper proves it is for ground term rewrite systems
following a conjecture made by Huet and Oppen in their survey.  We
also sketch an algorithm for checking this property. This algorithm is
based on tree automata and tree transducers. Here, we regard them as
rewrite systems and specialists in automata theory would translate
that easily in their language.},
comment={An extended version was published as ``Decidability of the
Confluence of Finite Ground Term Rewrite Systems and of Other Related
Term Rewrite Systems,'' {\em Information and Computation},
88(2):187--201, October 1990.}
}

                               3rd LICS
                           July 5--8, 1988
                         Edinburgh, Scotland

@InProceedings{KolaitisV88,
author={Phokion G. Kolaitis and Moshe Y. Vardi},
title={0-1 Laws and Decision Problems for Fragments of Second-Order
Logic},
pages={2--11},
crossref={LICS3},
comment={An extended version appeared in {\em Information and
Computation}, 87(1/2):301--337, July/August 1990.}
}

@InProceedings{ComptonL88,
author={Kevin L. Compton and Claude Laflamme},
title={An Algebra and a Logic for {$NC$}},
pages={12--21},
crossref={LICS3},
comment={An extended version appeared in {\em Information and
Computation}, 87(1/2):240--262, July/August 1990.}
}

@InProceedings{Tiomkin88,
author={M. Tiomkin},
title={Proving unprovability},
pages={22--26},
crossref={LICS3}
}

@InProceedings{HoareG88,
author={C. A. R. Hoare and M. J. C. Gordon},
title={Partial Correctness of {C-MOS} Switching Circuits: An Exercise
in Applied Logic},
pages={28--36},
crossref={LICS3}
}

@InProceedings{BruceL88,
author={Kim B. Bruce and Giuseppe Longo},
title={A Modest Model of Records, Inheritance and Bounded Quantification},
pages={38--50},
crossref={LICS3},
comment={An extended version appeared in {\em Information and
Computation}, 87(1/2):196--239, July/August 1990.}
}

@InProceedings{Amadio88,
author={Robert M. Amadio},
title={A fixed point extension of the second order lambda-calculus:
observable equivalences and models},
pages={51--60},
crossref={LICS3}
}

@InProceedings{GianniniR88,
author={Paola Giannini and Della Ronchi, Simona Ronchi},
title={Characterization of typings in polymorphic type discipline},
pages={61--70},
crossref={LICS3}
}

@InProceedings{KfouryTU88,
author={A. J. Kfoury and J. Tiuryn and P. Urzyczyn},
title={On the Computational Power of Universally Polymorphic Recursion},
pages={72--81},
crossref={LICS3}
}

@InProceedings{Breazu-Tannen88a,
author={Val Breazu-Tannen},
title={Combining Algebra and Higher-Order Types},
pages={82--90},
crossref={LICS3}
}

@InProceedings{BohmP88,
author={Corrado B{\"o}hm and Adolfo Piperno},
title={Characterizing {X}-Separability and One-Side Invertibility in
{$\lambda$}-{$\beta$}-{$\Omega$}-Calculus},
pages={91--101},
crossref={LICS3}
}

@InProceedings{DershowitzO88,
author={Nachum Dershowitz and Mitsuhiro Okada},
title={Proof-Theoretic Techniques for Term Rewriting Theory},
pages={104--111},
crossref={LICS3}
}

@InProceedings{KuperMPP88,
author={G. M. Kuper and K. W. McAloon and K. V. Palem and K. J. Perry},
title={Efficient Parallel Algorithms for Anti-Unification and Relative
Complement},
pages={112--120},
crossref={LICS3}
}

@InProceedings{BoudetJS88,
author={Alexandre Boudet and Jean-Pierre Jouannaud and Manfred
Schmidt-Schau{\ss}},
title={Unification in Free Extensions of {Boolean} Rings and {Abelian}
Groups},
pages={121-130},
crossref={LICS3}
}

@InProceedings{Wand88,
author={Mitchell Wand},
title={Corrigendum: Complete Type Inference for Simple Objects},
pages=132,
crossref={LICS3}
}

@InProceedings{DeganoNM88,
author={Pierpaolo Degano and Rocco De Nicola and Ugo Montanari},
title={On the Consistency of ``Truly Concurrent'' Operational and
Denotational Semantics (Extended Abstract)},
pages={133--141},
crossref={LICS3}
}

@InProceedings{Winskel88,
author={Glynn Winskel},
title={A Category of Labelled {Petri} Nets and Compositional Proof
System (Extended Abstract)},
pages={142--154},
crossref={LICS3},
comment={An extended version appeared as ``A compositional proof
system on a category of labelled transition systems,'' {\em
Information and Computation}, 87(1/2):2--57, July/August 1990}
}

@InProceedings{MeseguerM88,
author={Jos{\'e} Meseguer and Ugo Montanari},
title={{P}etri Nets Are Monoids: A New Algebraic Foundation for Net
Theory},
pages={155--164},
crossref={LICS3},
abstract={Petri nets are widely used to model concurrent systems.
However, their composition and abstraction mechanisms are inadequate:
we solve this problem in a satisfactory way.  We view place/transition
Petri nets as ordinary, directed graphs equipped with two algebraic
operations corresponding to parallel and sequential composition of
transitions.  A distributive law between the two operations captures a
basic fact about concurrency.  New morphisms are defined, mapping
single, atomic transitions into whole computations, thus relating
system descriptions at different levels of abstraction.  Categories
equipped with products and coproducts (corresponding to parallel and
nondeterministic computations) are introduced for Petri nets with and
without initial markings.  We briefly indicate how our approach also
yields function spaces and new interpretations of duality and
invariants.  These results provide a formal basis for expressing the
semantics of concurrent languages in terms of Petri nets.  They also
provide a new understanding of concurrency in terms of algebraic
structures over graphs and categories that should apply to other
models and contribute to the conceptual unification of concurrency.}
}

@InProceedings{AbadiL88,
author={Mart{\'\i}n Abadi and Leslie Lamport},
title={The Existence of Refinement Mappings},
pages={165--175},
crossref={LICS3}
}

@InProceedings{Dam88,
author={Mads Dam},
title={Relevance Logic and Concurrent Composition},
pages={178--185},
crossref={LICS3}
}

@InProceedings{Walker88,
author={D. J. Walker},
title={Bisimulations and Divergence},
pages={186--192},
crossref={LICS3}
}

@InProceedings{Cleaveland88,
author={Rance Cleaveland},
title={Priorities in Process Algebras},
pages={193--202},
crossref={LICS3},
comment={An extended version appeared in {\em Information and
Computation}, 87(1/2):58--77, July/August 1990.}
}

@InProceedings{LarsenT88,
author={Kim G. Larsen and Bent Thomsen},
title={A Modal Process Logic},
pages={203--210},
crossref={LICS3}
}

@InProceedings{Vorobyov88,
author={Sergey G. Vorobyov},
title={On the Arithmetic Inexpressiveness of Term Rewriting Systems},
pages={212-217},
crossref={LICS3}
}

@InProceedings{GallierSNP88,
author={J. Gallier and W. Snyder and P. Narendran and D. Plaisted},
title={Rigid {$E$}-Unification is {NP}-Complete},
pages={218--227},
crossref={LICS3},
comment={An extended version appeared as ``Rigid {$E$}-unification:
{NP}-completeness and applications to equational matings,'' {\em
Information and Computation}, 87(1/2):129--195, July/August 1990.}
}

@InProceedings{Bachmair88,
author={Leo Bachmair},
title={Proof by Consistency in Equational Theories},
pages={228--233},
crossref={LICS3}
}

@InProceedings{Meyer88,
author={Albert R. Meyer},
title={Semantical Paradigms: Notes for an Invited Lecture, with Two
Appendices by {S}tavros {S.} {C}osmadakis},
pages={236--253},
crossref={LICS3},
abstract={Comments on denotational semantics, highlighting ``goodness
of fit'' criteria between semantic domains and symbolic evaluators.
Two appendices provide the key parts of a long proof that Scott
domains give a {\em computationally adequate\/} and {\em fully
abstract\/} semantics for lambda calculus with simple {\em
recursive\/} types.}
}

@InProceedings{Coquand88,
author={Thierry Coquand},
title={Categories of Embeddings},
pages={256--263},
crossref={LICS3}
}

@InProceedings{Ehrhard88,
author={Thomas Ehrhard},
title={A Categorical Semantics of Constructions},
pages={264--273},
crossref={LICS3}
}

@InProceedings{FreydGSS88,
author={P. J. Freyd and J. Y. Girard and A. Scedrov and P. J. Scott},
title={Semantic Parametricity in Polymorphic Lambda Calculus},
pages={274--279},
crossref={LICS3}
}

@InProceedings{Bloom88,
author={Bard Bloom},
title={Can {LCF} Be Topped? {F}lat Lattice models of Typed Lambda
Calculus (Preliminary Report)},
pages={282--295},
crossref={LICS3},
comment={An extended version appeared in {\em Information and
Computation}, 87(1/2):263--300, July/August 1990.}
}

@InProceedings{CartwrightD88,
author={Robert Cartwright and Alan Demers},
title={The Topology of Program Termination},
pages={296--308},
crossref={LICS3}
}

@InProceedings{GunterJ88,
author={Carl A. Gunter and Achim Jung},
title={Coherence and Consistency in Domains (Extended Outline)},
pages={309--317},
crossref={LICS3}
}

@InProceedings{GerthCLS88,
author={Rob Gerth and Michael Codish and Yossi Lichtenstein and Ehud
Schapiro},
title={Fully Abstract Denotational Semantics for Flat {Concurrent}
{Prolog}},
pages={320--335},
crossref={LICS3}
}

@InProceedings{Baudinet88,
author={Marianne Baudinet},
title={Proving Termination Properties of {\sc prolog} Programs: A
Semantic Approach},
pages={336--347},
crossref={LICS3}
}

@InProceedings{Maher88,
author={Michael J. Maher},
title={Complete Axiomatizations of the Algebras of Finite, Rational
and Infinite Trees},
pages={348--357},
crossref={LICS3}
}

@InProceedings{ConstableS88,
author={Robert L. Constable and Scott Fraser Smith},
title={Computational Foundations of Basic Recursive Function Theory},
pages={360--371},
crossref={LICS3}
}

@InProceedings{Griffin88,
author={Timothy G. Griffin},
title={Notational definition---a formal account},
pages={372--383},
crossref={LICS3}
}

@InProceedings{SalvesenS88,
author={Anne Salvesen and Jan M. Smith},
title={The Strength of the Subset Type in {Martin-L{\"o}f's} Type Theory},
pages={384--391},
crossref={LICS3}
}

@InProceedings{MendlerA88,
author={Paul F. Mendler and Peter Aczel},
title={The notion of a {F}ramework and a framework for {LTC}},
pages={392--399},
crossref={LICS3},
abstract={A precise notion of a formal framework, meant to capture the
intuition of an open-ended range of deductive interpreted languages,
is proposed.  A particular framework, the Logical Theory of
Constructions, is developed by way of example.}
}

@InProceedings{Niwinski88,
author={Damian Niwi{\'n}ski},
title={Fixed Points vs.\ Infinite Generation},
pages={402--409},
crossref={LICS3}
}

@InProceedings{FaginHM88,
author={Ronald Fagin and Joseph Y. Halpern and Nimrod Megiddo},
title={A Logic for Reasoning about Probabilities},
pages={410--421},
crossref={LICS3},
comment={An extended version appeared in {\em Information and
Computation}, 87(1/2):78--128, July/August 1990.}
}

@InProceedings{MullerSS88,
author={David E. Muller and Ahmed Saoudi and Paul E. Schupp},
title={Weak Alternating Automata Give a Simple Explanation of Why Most
Temporal and Dynamic Logics are Decidable in Exponential Time},
pages={422--427},
crossref={LICS3}
}

@InProceedings{GrabowskiH88,
author={Micha{\l} Grabowski and Hardi Hungar},
title={On the Existence of Effective {Hoare} Logics},
pages={428--435},
crossref={LICS3}
}

			       4th LICS
			    June 5-8, 1989
	Asilomar Conference Center, Pacific Grove, California

@InProceedings{Scott89,
author={Scott, Dana S.},
title={Domains and Logics (Extended Abstract)},
crossref={LICS4},
pages={4--5},
note={Invited talk},
comment={No abstract.}
}

@InProceedings{Pitts89,
author={Pitts, Andrew M.},
title={Non-trivial Power Types Can't Be Subtypes of Polymorphic
Types},
crossref={LICS4},
pages={6--13},
abstract={
This paper establishes a new, limitative relation between the
polymorphic lambda calculus and the kind of higher-order type theory
which is embodied in the logic of toposes.  It is shown that any
embedding in a topos of the cartesian closed category of (closed)
types of a model of the polymorphic lambda calculus must place the
polymorphic types well away from the powertypes
$\sigma\rightarrow\Omega$ of the topos, in the sense that
$\sigma\rightarrow\Omega$ is a subtype of a polymorphic type only in
the case that $\sigma$ is empty (and hence $\sigma\rightarrow\Omega$
is terminal).  As corollaries, we obtain strengthenings of Reynolds'
result on the non-existence of set-theoretic models of polymorphism.}
}

@InProceedings{Moggi89,
author={Moggi, Eugenio},
title={Computational Lambda-Calculus and Monads},
crossref={LICS4},
pages={14--23},
abstract={
The $\lambda$-calculus is considered an useful mathematical tool in
the study of programming languages.  However, if one uses
$\beta\eta$-conversion to prove equivalence of programs, then a gross
simplification is introduced.  We give a calculus based on a
categorical semantics for {\em computations}, which provides a correct
basis for proving equivalence of programs, independent from any
specific computational model.},
comment={An extended version appeared as ``Notions of computation and
monads,'' {\em Information and Computation}, 93(1):55--92, July 1991.}
}

@InProceedings{Cosmadakis89,
author={Cosmadakis, Stavros S.},
title={Computing with Recursive Types (Extended Abstract)},
crossref={LICS4},
pages={24--38},
comment={No abstract.}
}

@InProceedings{Leivant89,
author={Leivant, Daniel},
title={Stratified Polymorphism (Extended Summary)},
crossref={LICS4},
pages={39--47},
abstract={
We consider a spectrum of predicative type abstraction disciplines
based on type quantification with stratified levels.  These lie in the
vast middle ground between parametric abstraction and full
impredicative abstraction. Stratified polymorphism has an attractive,
unproblematic, semantics, and has the potential of offering new
approaches to type inference, without sacrificing useful expressive
power.
\par
We show that the functions representable in the finitely-stratified
$\lambda$-calculus are precisely the super-elementary functions, ie
$\cal E_4$ in Grzegorczyk's subrecursive hierarchy.
\par
We also define methods of transfinite stratification, and we show that
stratification up to~$\omega^\omega$ has a simple finitary
representation, making it a potentially useful concept in programming
language design.  We prove that the functions representable by
stratified polymorphism up to~$\omega^\omega$ are precisely the
primitive-recursive functions.
\par
Finally, we point out that these results imply that the equality
problem for finitely stratified $\lambda$-calculus is not
super-elementary, and that the equality problem for the calculus
stratified up to~$\omega^\omega$ is not primitive recursive.},
comment={An extended version appeared as ``Finitely stratified
polymorphism,'' {\em Information and Computation}, 93(1):93--113, July
1991.}
}

@InProceedings{GaifmanS89b,
author={Gaifman, Haim and Shapiro, Ehud},
title={Proof Theory and Semantics of Logic Programs},
crossref={LICS4},
pages={50--62},
abstract={
We develop a resolution logic that is based on direct proofs rather
than on proofs by refutations.  The deductive system studied has
clauses as its formulas and resolution as the sole inference rule.
\par
We analyze this deductive system using a novel representation of
resolution proofs, called resolution graphs, and obtain a general
completeness theorem: a clause is a logical consequence of a set of
clauses iff it is either tautological or is subsumed by a clause
derivable from that set.  All previous completeness results for
resolution and its variants concerned either refutations or the
derivability of atoms.  Our completeness theorem generalizes these
results (including strong completeness of SLD resolution) to clauses.
\par
Proof-theoretic distinctions in resolution logic are much finer than
distinctions based on logical equivalence.  For example, from a
contradiction (the empty clause) nothing but the empty clause itself
is derivable; a clause derivable from the set of clauses must be in
the vocabulary of that set, thus generally not all tautologies are
derivable.
\par
In a previous paper~\cite{GaifmanS89a} we provided a framework for
studying the relations between observables, compositions, and fully
abstract semantics.  Within this framework we developed a
model-theoretic compositional semantics for logic programs, and
investigated the fully abstract equivalences induced by various
notions of composition.  This paper continues that study using the
proof theory of resolution logic.  This proof theory gives rise to
various semantics for logic programs that reflect more operational
details than does the model-theoretic semantics.  The basic one is the
answer substitution semantics~\cite{FalaschiLMP88} which distinguishes
between logically equivalent programs that may give different answer
substitutions to the same goal.  We show that taking answer
substitutions as observables is equivalent to taking the set of
derivable atoms, extend this basic semantics to various forms of
program composition, and obtain fully abstract invariants for these
compositions.}
}

@InProceedings{Fitting89,
author={Fitting, Melvin},
title={Negation As Refutation},
crossref={LICS4},
pages={63--70},
abstract={
A refutation mechanism is introduced into logic programming, dual to
the usual proof mechanism; then negation is treated via refutation.  A
four-valued logic is appropriate for the semantics: true, false,
neither, both.  In consistent programs are allowed, but
inconsistencies remain localized.  The four-valued logic is a
well-known one, due to Belnap, and is the simplest example of
Ginsberg's bilattice notion.  An efficient implementation based on
semantic tableaux is sketched; it reduces to SLD resolution when
negations are not involved.  The resulting system can give reasonable
answers to queries that involve both negation and free variables.
Also it gives the same results as Prolog when there are no negations.
Finally, an implementation in Prolog is given.}
}

@InProceedings{AbiteboulV89,
author={Abiteboul, Serge and Vianu, Victor},
title={Fixpoint Extensions of First-Order Logic and {D}atalog-Like
Languages},
crossref={LICS4},
pages={71--79},
abstract={
Datalog extensions with fixpoint semantics motivated by database
queries and updates are studied.  They suggest new non-trivial
fixpoint extensions of first-order logic with non-deterministic and/or
non-inflationary semantics.  Certain properties of $FO+IFP$ such as
the collapse of the hierarchy (based on the nesting of fixpoints) or
the existential normal form, hold for these various logics.  Their
expressive power is characterized.}
}

@InProceedings{BoseCLM89,
author={Bose, Soumitra and Clarke, Edmund M. and Long, David E. and
Michaylov, Spiro},
title={{PARTHENON}: A Parallel Theorem Prover for Non-{H}orn Clauses},
crossref={LICS4},
pages={80--89},
abstract={
We describe a parallel resolution theorem prover, called {\em
Parthenon}, that handles full first order logic.  Although there has
been much work on parallel implementations of logic programming
languages, Parthenon is apparently the first general purpose theorem
prover to be developed for a multiprocessor.  The system is based on a
modification of Warren's SRI model for or-parallelism and implements a
variant of Loveland's model elimination procedure.  It has been
evaluated on various shared memory multiprocessors including a
16-processor Encore Multimax.  We have found that typical theorem
proving problems exhibit a great deal of potential parallelism.
Parthenon has been able to exploit much of this parallelism, producing
both impressive absolute run times and near-linear speedup curves.}
}

@InProceedings{Wand89,
author={Wand, Mitchell},
title={Type Inference for Record Concatenation and Multiple
Inheritance},
crossref={LICS4},
pages={92--97},
abstract={
We show that the type inference problem for a lambda calculus with
records, including a record concatenation operator, is decidable.  We
show that this calculus does not have principal types, but does have
finite complete sets of types: that is, for any term $M$ in the
calculus, there exists an effectively generable finite set of type
schemes such that every typing for $M$ is an instance of one the
schemes in the set.
\par
We show how a simple model of object-oriented programming, including
hidden instance variables and multiple inheritance, may be coded in
this calculus.  We conclude that type inference is decidable for
object-oriented programs, even with multiple inheritance and classes
as first-class values.},
comment={An extended version appeared in {\em Information and
Computation}, 93(1):1--15, July 1991.}
}

@InProceedings{KfouryTU89,
author={Kfoury, A. J. and Tiuryn, J. and Urzyczyn, P.},
title={Computational Consequences and Partial Solutions of a
Generalized Unification Problem (Partial Report)},
crossref={LICS4},
pages={98--105},
comment={No abstract.}
}

@InProceedings{Robinson89,
author={Robinson, Edmund},
title={How Complete is {PER}?},
crossref={LICS4},
pages={106--111},
abstract={
The category of partial equivalence relations on the natural numbers
({\sf PER}) has been used extensively in recent years to model various
forms of higher-order type theory.  It is well-known that {\sf PER}
can be viewed as a category of sets in a non-standard model of
intuitionistic Zermelo-Fraenkel set theory.  The use of {\sf PER} as a
vehicle for modelling type theory then arises from completeness
properties of this category.  The purpose of this paper is to
demonstrate these completeness properties, and to show that,
constructively, some complete categories are more complete than
others.}
}

@InProceedings{Breazu-TannenCGS89,
author={Breazu-Tannen, V. and Coquand, T. and Gunter, C. A. and
Scedrov, A.},
title={Inheritance and Explicit Coercion (Preliminary Report)},
crossref={LICS4},
pages={112--129},
abstract={
We present a method for providing semantic interpretations for
languages which feature {\em inheritance\/} in the framework of
statically checked, rich type disciplines.  We illustrate our approach
on an extension of the language Fun of Cardelli and Wegner, which we
interpret via a translation into an extended polymorphic lambda
calculus.  Our approach interprets inheritances in Fun and {\em
coercion functions\/} already {\em definable\/} in the target of the
translation.  Existing techniques in the theory of semantic domains
can be then used to interpret the extended polymorphic lambda
calculus, thus providing many models for the original language.  Our
method allows the simultaneous modeling of {\em parametric
polymorphism}, {\em recursive types}, and {\em inheritance}, something
that was regarded as problematic because of the seemingly
contradictory characteristics of inheritance and type recursion on
higher types.
\par
We identify the main difficulty in providing interpretations for
explicit type disciplines featuring inheritance, namely that programs
can type-check in more than one way.  Since interpretations follow the
type-checking derivations, {\em coherence\/} theorems are required,
(that is, one must prove that the meaning of a program does not depend
on the way it was type-checked), and we do prove them for our semantic
method.  Interestingly, proving coherence in the presence of recursive
types, variants, and abstract types forced us to reexamine fundamental
equational properties that arise in proof theory (in the form of
commutative reductions) and domain theory (in the form of strict {\em
vs}.\ non-strict functions).},
comment={An extended version appeared in {\em Information and
Computation}, 93(1):172--221, July 1991.}
}

@InProceedings{Davis89,
author={Davis, Martin},
title={{E}mil {P}ost's Contributions to Computer Science},
crossref={LICS4},
pages={134--136},
note={Invited talk},
abstract={
The work of the mathematical logician Emil Post is surveyed from the
point of view of its relevance for computer science.}
}

@InProceedings{AcetoH89,
author={Aceto, L. and Hennessy, M.},
title={Towards Action-Refinement in Process Algebras},
crossref={LICS4},
pages={138--145},
abstract={
We present a simple process algebra which supports a form of
refinement of an action by a process and address the question of an
appropriate equivalence relation for it.  The main result of the paper
is that an adequate equivalence can be defined in a very intuitive
manner and moreover can be axiomatized in much the same way as the
standard behavioural equivalences.}
}

@InProceedings{Gischer89,
author={Gischer, Jay L.},
title={A Small Universal Model for System Executions},
crossref={LICS4},
pages={146--153},
abstract={
Lamport has introduced a language for concurrency which uses two
relations, strong (temporal) precedence, and weak (causal) precedence.
Systems of concurrent activities under this scheme are called System
Executions.  We show that every consistent set of atomic relations has
a unified model of size roughly $O(n^2)$.  This model can be used to
give a simplified proof of completeness of some axioms.  We give
several complexity results for deciding the theory of several classes
of axiom sets, for both partial models and global-time models, showing
many such variations to have the same complexity as transitive closure
or matrix multiplication.  Finally, we show that deciding disjunctive
axioms is NP-complete, for both global-time and the standard model.}
}

@InProceedings{Moschovakis89,
author={Moschovakis, Yiannis N.},
title={A Game-Theoretic Modeling of Concurrency},
crossref={LICS4},
pages={154--163},
abstract={
We introduce in this paper a model for asynchronous, concurrent
communication, where each agent's {\em perception\/} of the system is
represented by a game of interaction.  The model combines (strict)
fair merge with full recursion, and the main mathematical results
provide evidence for the robustness and naturalness of our
interpretation of recursive definitions of non-deterministic
processes.  Our approach is closest to Park's, whose ideas
in~\cite{Park80,Park83} are the starting points for this work.},
comment={An extended version appeared as ``A model of concurrency with
fair merge and full recursion,'' {\em Information and Computation},
93(1):114--171, July 1991.}
}

@InProceedings{RabinovichT89,
author={Rabinovich, Alexander Moshe and Trakhtenbrot, Boris A.},
title={Nets and Data Flow Interpreters},
crossref={LICS4},
pages={164--174},
abstract={
We investigate and compare two ways of specifying stream relations (in
particular---stream functions).
\par
The first one uses relational programs, i.e. netlike program schemes
in which the signature primitives are interpreted as relations over a
given CPO.  No stream domains are assumed; semantics is in fixed point
style.
\par
The second one is through data flow nets i.e., nets whose nodes are
interpreted as processes (computational stations).
\par
We prove the existence of an adequate data flow interpreter for
relational programs over all relations (not only functional) and
(essentially) its uniqueness.  When dealing with functions the
interpreter is modular and obeys the Kahn Principle.
\par
On the other hand analyzing the deviations from Kahn's Principle we
identify two kinds of anomalies:
\par
The first one (``meagerness'' anomaly) is caused by the defect of the
used processes (computational stations) and holds in fact for
arbitrary (even for very simple functional) input-output behaviors.
This anomaly may always be avoided through the use of appropriate
processes.
\par
The second (``ambiguity'' anomaly) is rooted in the semantics of
relational nets over arbitrary CPO (and not specifically over stream
domains).  It is unavoidable in any extension beyond functional
behaviors.}
}

@InProceedings{DeganoMM89,
author={Degano, Pierpaolo and Meseguer, Jos{\'e} and Montanari, Ugo},
title={Axiomatizing Net Computations and Processes},
crossref={LICS4},
pages={175--185},
abstract={
Descriptions of concurrent behaviors in terms of partial orderings
(called {\em nonsequential processes\/} or simply {\em processes\/} in
Petri net theory) have been recognized as superior when information
about distribution in space, about causal dependency or about fairness
must be provided.  However, at least in the general case of
Place/Transition (P/T) nets, the proposed models lack a suitable,
general notion of {\em sequential composition}.
\par
In this paper, a new algebraic axiomatization is proposed, where,
given a net $N$, a term algebra ${\cal P}[N]$ with two operations of
parallel and sequential composition is defined.  The congruence
classes generated by a few simple axioms are proved isomorphic to a
slight refinement of classical processes.
\par
Actually, ${\cal P}[N]$ is a symmetric monoidal category, parallel
composition is the monoidal operation on morphisms and sequential
composition is morphism composition.  Besides ${\cal P}[N]$, we
introduce a category ${\cal S}[N]$ containing the classical occurrence
and step sequences.  The term algebras of ${\cal P}[N]$ and of ${\cal
S}[N]$ are in general incomparable, and thus we introduce two more
categories ${\cal K}[N]$ and ${\cal T}[N]$ providing a most concrete
and a most abstract extremum respectively.  A simple axiom expressing
the functoriality of parallel composition allows us to map ${\cal
K}[N]$ to ${\cal P}[N]$ and ${\cal S}[N]$ to ${\cal T}[N]$, while
commutivity of parallel composition maps ${\cal K}[N]$ to ${\cal
S}[N]$ and ${\cal P}[N]$ to ${\cal T}[N]$\ldots.
\par
Morphisms of ${\cal K}[N]$ constitute a new notion of concrete net
computation, while the strictly symmetric monoidal category ${\cal
T}[N]$ was introduced previously by two of the authors as a new
algebraic foundation for P/T nets~\cite{MeseguerM88}.  In this paper,
the morphisms of ${\cal T}[N]$ are proved isomorphic to the processes
recently defined in terms of the ``swap'' transformation by Best and
Devillers~\cite{BestD87}.  Thus the diamond of the four category gives
a full account in algebraic terms of the relations between
interleaving and partial ordering observations of P/T net
computations.}
}

@InProceedings{JonesP89,
author={Jones, C. and Plotkin, G. D.},
title={A Probabilistic Powerdomain of Evaluations},
crossref={LICS4},
pages={186--195},
abstract={
We give a probabilistic powerdomain construction on the category of
inductively complete partial orders; it is the partial order of
continuous $[0,1]$-valued evaluations on the Scott topology.  By means
of a theory of integration with respect to such evaluations, the
powerdomain is shown to be a monad, and indeed one gets a model for
Moggi's computational lambda-calculus.  One can also solve recursive
domain equations involving the powerdomain, and all this gives a
meta-language for programming languages with probabilistic features.
This is used to give the semantics of a language with a probabilistic
parallel construct.  We show the construction generalises previous
work on partial orders of measures, and indeed restricts to the
category of continuous partial orders, where it can be characterised
as a free continuous finitary algebra.}
}

@InProceedings{Howe89,
author={Howe, Douglas J.},
title={Equality In Lazy Computation Systems},
crossref={LICS4},
pages={198--203},
abstract={
In this paper we introduce a general class of lazy computation systems
and define a natural program equivalence for them.  We prove that if
an {\em extensionality\/} condition holds of each of the operators of
a computation system, then the equivalence relation is a congruence,
so that the usual kinds of equality reasoning are valid for it.  This
condition is a simple syntactic one, and is easy to verify for the
various lazy computation system we have considered so far.  We also
give conditions under which the equivalence coincides with
observational congruence.  These results have some important
consequences for type theories like those of Martin-L\"of and Nuprl.}
}

@InProceedings{Vrijer89,
author={{de Vrijer}, Roel},
title={Extending the Lambda Calculus with Surjective Pairing is
Conservative},
crossref={LICS4},
pages={204--215},
abstract={
We consider the equational theory $\bf\lambda\pi$ of
$\lambda$-calculus extended with constants $\pi$, $\pi_0$, $\pi_1$ and
axioms for surjective pairing: $\pi_0(\pi XY)=X$, $\pi_1(\pi XY)=Y$,
$\pi(\pi_0X)(\pi_1X)=X$.  The reduction system that one obtains by
reading the equations as reductions (from left to right) is not
Church-Rosser.  Despite of this failure, we obtain a syntactic
consistency proof of $\bf\lambda\pi$.  Moreover, it is shown that
$\bf\lambda\pi$ is a conservative extension of the pure
$\lambda$-calculus.}
}

@InProceedings{AbadiPP89,
author={Abadi, Mart{\'\i}n and Pierce, Benjamin and Plotkin, Gordon},
title={Faithful Ideal Models for Recursive Polymorphic Types},
crossref={LICS4},
pages={216--225},
abstract={
We explore ideal models for a programming language with recursive
polymorphic types, variants of the model studied by MacQueen, Plotkin
and Sethi.  The use of suitable ideals yields a close fit between
models and programming language.  Two of our semantics of type
expressions are faithful, in the sense that programs that behave
identically in all contexts have exactly the same types.}
}

@InProceedings{HarperST89,
author={Harper, Robert and Sannella, Donald and Tarlecki, Andrzei},
title={Structure and Representation in {LF}},
crossref={LICS4},
pages={226--237},
abstract={
The purpose of a logical framework such as LF is to provide a language
for defining logical systems suitable for use in a logic-independent
proof development environment.  All inferential activity is an object
logic (in particular, proof search) is to be conducted in the logical
framework via the representation of that logic in the framework.  An
important tool for controlling search in an object logic is the use of
structured theory presentations.  In order to apply these ideas to the
setting of a logical framework, we study the behavior of structured
theory presentations under representation in a framework, focusing on
the problem of ``lifting'' presentations from the object logic to the
metalogic of the framework.  We also consider imposing structure on
logic presentations so that logical systems may themselves be defined
in a modular fashion.  This opens the way to a CLEAR-like language for
defining both theories and logics in a logical framework.}
}

@InProceedings{Lifschitz89,
author={Lifschitz, Vladimir},
title={The Mathematics of Nonmonotonic Reasoning (Abstract)},
crossref={LICS4},
pages=242,
note={Invited talk}
}

@InProceedings{Vardi89,
author={Vardi, Moshe Y.},
title={On the Complexity of Epistemic Reasoning},
crossref={LICS4},
pages={243--252},
abstract={
A fundamental problem with epistemic logics based on Hintikka's
possible-worlds semantics is the logical omniscience problem.  A
partial solution to the problem is to use Montague and Scott's
approach to modal logic; in that approach agent's knowledge is
characterized not by a set of possible worlds but rather by a set of
propositions known by the agent.  By imposing various closure
conditions on the set of propositions known by the agent, we can model
agents with different reasoning powers.
\par
In this paper we study the complexity of the decision problem for
epistemic logics based on Montague and Scott's semantics.  We are
mainly interested in finding out how assumptions about the agents'
reasoning power affects the complexity of reasoning about the agents'
knowledge.  We study a spectrum of assumptions and show that the
complexity of the logic under different assumptions is always in NP or
PSPACE. Furthermore, we seem to pinpoint the ``mental faculty'' that
raises the complexity of the logic from NP to PSPACE; it is the
ability to combine distinct items of knowledge, namely, to infer from
the facts $p$ and $q$ the fact $p\wedge q$.}
}

@InProceedings{KiferL89,
author={Kifer, Michael and Lozinskii, Eliezer L.},
title={{RI}: A Logic for Reasoning with Inconsistency},
crossref={LICS4},
pages={253--262},
abstract={
Most known computational approaches to reasoning have problems when
facing inconsistency, so they assume that a given logical system is
consistent.  Unfortunately, the latter is difficult to verify and very
often is not true.  It may happen that addition of a data to a large
system makes it inconsistent, and hence destroys the vast amount of
meaningful information.  We present a logic, called RI (Reasoning with
Inconsistency), that treats any set of clauses, either consistent or
not, in a uniform way.  In this logic, consequences of a contradiction
are not nearly as damaging as in the standard predicate calculus, and
meaningful information can still be extracted from an inconsistent set
of formulae.  RI has a resolution-based sound and complete proof
procedure.  It is a much richer logic than the predicate calculus, and
the latter can be imitated within RI in several ways (depending on the
intended meaning of the predicate calculus formulae).  We also
introduce a novel notion of ``epistemic entailment'' and show its
importance for investigating inconsistency in the predicate calculus.}
}

@InProceedings{MisloveMO89,
author={Mislove, Michael W. and Moss, Lawrence S. and Oles, Frank J.},
title={Non-Well-Founded Sets Obtained from Ideal Fixed Points},
crossref={LICS4},
pages={263--272},
abstract={
Motivated by ideas from the study of abstract data types, we show how
to interpret non-well-founded sets as fixed points of continuous
transformations of an initial continuous algebra.  We consider a
preordered structure closely related to the set HF of well-founded,
hereditarily finite sets.  By taking its ideal completion, we obtain
an initial continuous algebra in which we are able to solve all of the
usual systems of equations that characterize hereditarily finite,
non-well-founded sets.  In this way, we are able to obtain a structure
which is isomorphic to $\rm HF_1$, the non-well-founded analog of
HF.},
comment={An extended version appeared as ``Non-well-founded sets
modeled as ideal fixed points,'' {\em Information and Computation},
93(1):16--54, July 1991.}
}

@InProceedings{Fernando89,
author={Fernando, R. T. P},
title={On Substitutional Recursion Over Non-Well-Founded Sets},
crossref={LICS4},
pages={273--282},
comment={No abstract.}
}

@InProceedings{MasonT89,
author={Mason, Ian A. and Talcott, Carolyn},
title={Axiomatizing Operational Equivalence in the Presence of Side
Effects},
crossref={LICS4},
pages={284--293},
abstract={A formal system is presented for deriving assertions about
programs with effects.  Programs are expressions of a first-order
Scheme- or Lisp-like language.  The formal system defines a
single-conclusion consequence relation finite sets of constraints and
assertions of the form `e is undefined' or `e0 is equivalent to e1'.
A constraint is an atomic or negated atomic formula in the first-order
language consisting of equality, selectors, and tests for atomicity.
The semantics of the formal system is given by a semantic consequence
relation which is defined in terms of a class of memory models for
assertions and constraints.  The main results of this paper are that
the deduction system is sound and complete with respect to the
semantics.  [Note: This abstract did not appear in the original
conference paper; it was supplied by the authors for this bibliography.]},
comment={Extended version to appear as ``Inferring the Equivalence of
Functional Programs That Mutate Data,'' {\em Theoretical Computer
Science}, vol 103, 1993.}
}

@InProceedings{JagadeesanPP89,
author={Jagadeesan, Radha and Panangaden, Prakash and Pingali,
Keshav},
title={A Fully Abstract Semantics for a Functional Language with Logic
Variables},
crossref={LICS4},
pages={294--303},
abstract={
There is much interest in the declarative languages community in
integrating logic variables into functional languages.  In this paper,
we give a full semantic account of such a language.  We present a
Plotkin-style operational semantics for the language and an abstract
semantics that expresses meanings as closure operators on a Scott
domain.  We also show that the denotational semantics is fully
abstract with respect to the operational semantics.}
}

@InProceedings{Mosses89a,
author={Mosses, Peter D.},
title={Unified Algebras and Institutions},
crossref={LICS4},
pages={304--312},
abstract={
A novel framework for algebraic specification of abstract data types
is introduced.  It involves so-called ``unified algebras'', where
sorts are treated as values, so that operations may be applied to
sorts as well as to the elements that they classify.
\par
An institution for unified algebras is defined, and shown to be
liberal.  However, the ordinary ``forgetful'' functor does not forget
any values in unified algebras, so the usual data constraints do not
have any models.  A ``more forgetful'' functor is introduced and used
to define so-called ``bounded'' data constraints, which have the
expected models.}
}

@InProceedings{Pfenning89,
author={Pfenning, Frank},
title={{E}lf: A Language for Logic Definition and Verified
Metaprogramming},
crossref={LICS4},
pages={313--322},
abstract={
We describe Elf, a metalanguage for proof manipulation environments
that are independent of any particular logic system.  Elf is intended
for meta-programs such as theorem provers, proof transformers, or type
inference programs for programming languages with complex type
systems.  Elf unifies logic definition (in the style of LF, the
Edinburgh Logical Framework) with logic programming (in the style of
$\lambda$Prolog).  It achieves this unification by giving {\em
types\/} an operational interpretation, much the same way that Prolog
gives certain formulas (Horn-clauses) an operational interpretation.
Novel features of Elf include: (1)~the Elf search process
automatically constructs terms that can represent object-logic proofs,
and thus a program need not construct them explicitly, (2)~the
partial correctness of meta-programs with respect to a given logic can
be expressed and proved in Elf itself, and (3)~Elf exploits Elliott's
unification algorithm for a $\lambda$-calculus with dependent types.}
}

@InProceedings{Stolboushkin89,
author={Stolboushkin, Alexey P.},
title={Some Complexity Bounds for Dynamic Logics},
crossref={LICS4},
pages={324--332},
abstract={
It is considered the class $\cal G$ of Adian's structures with
pairwise different exponents.  It is known that both {\em DDL\/} and
{\em CF-DDL\/} dynamic logics have unwind property in every
structure~$\Gamma$ in~$\cal G$, thus they are equivalent in~$\Gamma$
to first-order logic.  Nonetheless, it turns out that these three
logics have in the class~$\cal G$ different complexity bounds.  The
main result is to prove polynomial upper bounds for {\em DDL\/}
formulae.  A a corollary we have that {\em DDL\/} and {\em CF-DDL\/}
are unequivalent in~$\cal G$ to one another.  The proof remains valid
even in the presence of elementary tests and rich tests.}
}

@InProceedings{EmersonJ89,
author={Emerson, E. Allen and Jutla, Charanjit S.},
title={On Simultaneously Determinizing and Complementing
$\omega$-Automata (Extended Abstract)},
crossref={LICS4},
pages={333--342},
abstract={
We give a construction to simultaneously determinize and complement a
Buchi Automaton on Infinite strings, with an exponential blowup in
states, and linear blowup in number of pairs.  An exponential lower
bound is already known.  The previous best construction was double
exponential (Safra~88).  This permits exponentially improved
essentially optimal decision procedures for various Modal Logics of
Programs.  The new construction also gives exponentially improved
conversions between various kinds of $\omega$-automata.}
}

@InProceedings{Lubarsky89,
author={Lubarsky, Robert S.},
title={{$\mu$}-Definable Sets of Integers},
crossref={LICS4},
pages={343--352},
abstract={
The $\mu$-calculus is a language consisting of standard first-order
finitary logic with a least fixed point operator applicable to
positive inductive definitions.  The main theorem of this paper is a
set-theoretic characterization of the sets of integers definable in
the $\mu$-calculus.  Another theorem used but not proven here is a
prenex normal form theorem for the $\mu$-calculus.}
}

@InProceedings{ClarkeLM89,
author={Clarke, E. M. and Long, D. E. and McMillan, K. L.},
title={Compositional Model Checking},
crossref={LICS4},
pages={353--362},
abstract={
We describe a method for reducing the complexity of temporal logic
model checking in systems composed of many parallel processes.  The
goal is to check properties of the components of a system and then
deduce global properties from these local properties.  The main
difficulty with this type of approach is that local properties are
often not preserved at the global level.  We present a general
framework for using additional {\em interface processes\/} to model
the environment for a component.  These interface processes are
typically much simpler than the full environment of the component.  By
composing a component with its interface processes and then checking
properties of this composition, we can guarantee that these properties
will be preserved at the global level.  We give two example
compositional systems based on the logic CTL*.}
}

@InProceedings{Goerdt89,
author={Goerdt, Andreas},
title={Characterizing Complexity Classes By Higher Type Primitive
Recursive Definitions},
crossref={LICS4},
pages={364--374},
abstract={
Higher type primitive recursive definitions (also known as G\"odel's
system T) defining first-order functions (i.e. functions of type
$i\times\ldots\times i\rightarrow i,i$ for individuals, such
definitions have higher types in between) can be classified into an
infinite hierarchy: A definition is in the $n$'th level of this
hierarchy, a so called rank-$n$-definition iff $n$ is an upper bound
on the levels of the types occurring in it.
\par
We interpret these definitions over finite structures and show:
Rank-2-definitions characterize (in the sense of~\cite{Gurevich83},
say) PTIME, rank-3-definitions characterize PSPACE, rank-4-definitions
characterize EXPTIME ($={\rm DTIME}(2^{\rm poly})$).  This extends the
result of~\cite{Gurevich83} saying, rank-1 primitive recursive
definitions in finite structures characterize LOGSPACE.}
}

@InProceedings{NerodeRS89,
author={Nerode, A. and Remmel, J. B. and Scedrov, A.},
title={Polynomially Grade Logic~{I}: A Graded Version of System~{T}},
crossref={LICS4},
pages={375--395},
abstract={
We investigate a logical framework for programming languages which
treats requirements on computational resources as part of the formal
program specification.  Resource bounds are explicit in the syntax of
all programs.  In a programming language based on this approach,
compliance of a program with imposed resource bounds would be assured
by verifying the syntactic correctness using a compiler with a static
type checking feature.  The principal innovation of this paper is the
introduction of systems of logical inference, called polynomially
graded logics.  These logics make resource bounds part of every
proposition and every deduction.  The sample calculus presented in
this paper is a restriction of G\"odel's system T to polynomial time
resources.  We prove that the numerical functions representable in
this calculus are exactly the PTIME functions.}
}

@InProceedings{Luo89,
author={Luo, Zhaohui},
title={{{\bf ECC}}, an Extended Calculus of Constructions},
crossref={LICS4},
pages={386--395},
abstract={
We present a higher-order calculus {\bf ECC} which can be seen as an
extension of the calculus of constructions~\cite{CoquandH88} by adding
strong sum types and a fully cumulative type hierarchy.  {\bf ECC}
turns out to be rather expressive so that mathematical theories can be
abstractly described and abstract mathematics may be adequately
formalized.  It is shown that {\bf ECC} is strongly normalizing and
has other nice proof-theoretic properties.  An $\omega$-{\bf Set}
(realizability) model is described to show how the essential
properties of the calculus can be captured set-theoretically.}
}

@InProceedings{Middeldorp89,
author={Middeldorp, Aart},
title={A Sufficient Condition for the Termination of the Direct Sum of
Term Rewriting Systems},
crossref={LICS4},
pages={396--401},
abstract={
We prove a conjecture by Rusinowitch stating that the direct sum of
two terminating term rewriting systems is terminating if one of the
systems contains neither collapsing nor duplicating rules.}
}


			       5th LICS
			    June 4-7, 1990
		      Philadelphia, Pennsylvania

@inproceedings{KfouryT90,
author={Kfoury, A. J. and Tiuryn, J.},
title={Type Reconstruction in Finite-Rank Fragments of the Polymorphic
{$\lambda$}-Calculus (Extended Summary)},
crossref={LICS5},
pages={2--11},
abstract={
We prove that the problem of type reconstruction in the polymorphic
$\lambda$-calculus of rank~2 is polynomial-time equivalent to the
problem of type reconstruction in {\bf ML}, and is therefore
DEXPTIME-complete.  We also prove that for every $k>2$, the problem of
type reconstruction in the polymorphic $\lambda$-calculus of rank~$k$,
extended with suitably chosen constants with types of rank~1, is
undecidable.},
comment={An extended version appeared in {\em Information and
Computation}, 98(2):228--257, June 1992.}
}


@inproceedings{RobinsonR90,
author={Robinson, Edmund and Rosolini, Giuseppe},
title={Polymorphism, Set Theory, and Call-by-Value},
crossref={LICS5},
pages={12--18},
abstract={
We discuss set-theoretic (or rather the more general topos-theoretic)
models of polymorphic lambda-calculi under the assumption that the
datatypes of the language are to be interpreted as sets, and the
operations as partial functions.  We show that it is not possible to
obtain a model in which function spaces are interpreted by the full
partial function space, but that it is nevertheless possible to have
models which incorporate a usefully large class of partial functions.}
}

@inproceedings{DrosteG90,
author={Droste, Manfred and G{\"o}bel, R{\"u}diger},
title={Universal Domains in the Theory of Denotational Semantics of
Programming Languages},
crossref={LICS5},
pages={19--34},
comment={no abstract}
}

@inproceedings{Jung90,
author={Jung, Achim},
title={The Classification of Continuous Domains (Extended Abstract)},
crossref={LICS5},
pages={35--40},
abstract={
The long-standing problem of finding the maximal cartesian closed
categories of continuous domains is solved.  The solution requires the
definition of a new class of continuous domains, called {\em
FS-domains}, which contains all retracts of SFP-objects.  The
properties of FS-domains are discussed in some detail.}
}

@inproceedings{HeintzeJ90b,
author={Heintze, Nevin and Jaffar, Joxan},
title={A Decision Procedure for a Class of Set Constraints (Extended
Abstract)},
crossref={LICS5},
pages={42--51},
abstract={
A set constraint is of the form ${\it exp}_1\supseteq{\it exp}_2$,
where ${\it exp}_1$ and ${\it exp}_2$ are set expressions constructed
using variables, function symbols, projection symbols, and the set
union, intersection and complement symbols.  While the satisfiability
problem for such constraints is open, restricted classes have been
useful in program analysis.  The main result herein is a decision
procedure for {\em definite\/} set constraints which are of the
restricted form $a\supseteq{\it exp}$ where $a$ contains only
constants, variables and function symbols, and ${\it exp}$ is a
positive set expression (that is, it does not contain the complement
symbol).  A conjunction of such constraints, whenever satisfiable, has
a least model and the algorithm will output an explicit representation
of this model.
\par
An additional feature of the algorithm is that it deals with another
important class of set constraints.  These are the {\em solved form\/}
set constraints which have the form $X_1={\it exp}_1$, $\cdots$,
$X_n={\it exp}_n$ where the $X_i$ are distinct variables and the ${\it
exp}_i$ are positive set expressions.  A solved form constraint is
always satisfiable and possesses a least and greatest model.  Our
algorithm can output explicit representations of both.}
}

@inproceedings{Lassez90,
author={Lassez, Jean-Louis},
title={A Constraint Sequent Calculus},
crossref={LICS5},
pages={52--61},
abstract={
Constraints play an important role in programming languages and in OR
and AI work.  Here we give an axiomatic approach that accounts for
examples that come up in logic programming, symbolic computation,
affine geometry and elsewhere.  We show that if disjunction behaves in
an intuitionistic fashion, notions of canonical form for positive
constraints can be systematically extended to include negative
constraints.  As a consequence, completeness theorems involving
positive and negative constraints can be proven in a general setting
for constraint propagation.}
}

@inproceedings{Comon90,
author={Comon, Hubert},
title={Solving Inequations in Term Algebras (Extended Abstract)},
crossref={LICS5},
pages={62--69},
abstract={
We show that the existential fragment of the theory of a lexicographic
path ordering which extends a total precedence is decidable.}
}

@inproceedings{Meyden90,
author={van der Meyden, R.},
title={The Dynamic Logic of Permission},
crossref={LICS5},
pages={72--78},
abstract={
Intelligent legal information systems require the ability to represent
two different notions of permission, one of which, ``free choice''
permission, cannot be adequately represented in standard modal logics.
We define a logic which handles this modality by using ideas from
dynamic logic.  The main result is the completeness of an
axiomatization of the logic.}
}

@inproceedings{MarekNR90,
author={Marek, W. and Nerode, A. and Remmel, J.},
title={A Theory of Nonmonotonic Rule Systems},
crossref={LICS5},
pages={79--94},
comment={no abstract}
}

@inproceedings{AllenCHA90,
author={Allen, Stuart F. and Constable, Robert L. and Howe, Douglas J.
and Aitken, William E.},
title={The Semantics of Reflected Proof},
crossref={LICS5},
pages={95--105},
abstract={
We begin to lay the foundations for reasoning about proofs whose steps
include both invocations of programs to build subproofs ({\em
tactics\/}) and references and representations of proofs themselves
(reflected proofs).   The main result is the definition of a single
type of proof which can mention itself, using a new technique which
finds a fixed point of a mapping between metalanguage and object
language.  The single type contrasts with hierarchies of types used in
other approaches to accomplish the same classification.  We show that
these proofs are valid, and that every proof can be reduced to a proof
involving only primitive inference rules.  We also show how to extend
the results to proofs from which programs (such as tactics) can be
derived, and to proofs that can refer to a library of definitions and
previously proven theorems.  We believe that the mechanism of
reflection is fundamental in building proof development systems, and
we illustrate its power with applications to automating reasoning and
describing modes of computation.}
}

@inproceedings{LarsenX90,
author={Larsen, Kim Guldstrand and Xinxin, Liu},
title={Equation Solving Using Modal Transition Systems},
crossref={LICS5},
pages={108--117},
abstract={
This paper offers as its main contribution a complete treatment of
{\em equation solving\/} within process algebra\ldots for equation
systems of the following form:
$$C_1(X)\sim P_1,\ldots\ldots,C_n(X)\sim P_n\eqno(1)$$
where $C_i$ are arbitrary contexts (i.e. derived operators) of some
process algebra, $P_i$ are arbitrary process (i.e. terms of the
process algebra), $\sim$ is the bisimulation equivalence\ldots, and
$X$ is the unknown process to be found (if possible).  As our main
results we show that the solution set to~(1) may be characterized in
terms of a {\em Disjunctive Modal Transition System}, and that a
solution to~(1) may be readily extracted (when solutions exist) on
this basis.  In fact, our results have lead directly to an
implementation (in Prolog) of an automatic tool for solving equations
in the finite-state case.},
comment={Very long list of references elided from abstract.}
}

@inproceedings{NicolaV90a,
author={De Nicola, Rocco and Vaandrager, Frits},
title={Three Logics for Branching Bisimulation (Extended Abstract)},
crossref={LICS5},
pages={118--129},
abstract={
Three temporal logics are introduced which induce on labelled
transition systems the same identifications as branching bisimulation.
The first is an extension of Hennessy-Milner Logic with a kind of
``until'' operator.  The second is another extension of
Hennessy-Milner Logic which exploits the power of backward modalities.
The third is $\mbox{\rm CTL}^*$ without the next-time operator
interpreted over all paths, not just over maximal ones.  A relevant
side-effect of the last characterization is that it sets a bridge
between the state- and event-based approaches to the semantics of
concurrent systems.}
}

@inproceedings{GlabbeekSST90,
author={van Glabbeek, Rob and Smolka, Scott A. and Steffen, Bernhard
and Tofts, Chris M. N.},
title={Reactive, Generative, and Stratified Models of Probabilistic
Processes},
crossref={LICS5},
pages={130--141},
comment={no abstract.}
}

@inproceedings{Moller90,
author={Moller, Faron},
title={The Nonexistence of Finite Axiomatizations for {CCS}
Congruences},
crossref={LICS5},
pages={142--153}
}

@inproceedings{KolaitisV90,
author={Kolaitis, Phokion G. and Vardi, Moshe Y.},
title={0-1 Laws for Infinitary Logics (Preliminary Report)},
crossref={LICS5},
pages={156--167},
comment={An extended version appeared in {\em Information and
Computation}, 98(2):258--294, June 1992.}
}

@inproceedings{Kolaitis90,
author={Kolaitis, Phokion G.},
title={Implicit Definability on Finite Structures and Unambiguous
Computations (Preliminary Report)},
crossref={LICS5},
pages={168--180}
}

@inproceedings{Clote90,
author={Clote, Peter},
title={{ALOGTIME} and a Conjecture of {S}. {A}. {C}ook (Extended
Abstract)},
crossref={LICS5},
pages={181--189}
}

@inproceedings{Courcelle90,
author={Courcelle, Bruno},
title={On the Expression of Monadic Second-Order Graph Properties
Without Quantifications Over Sets of Edges (Extended Abstract)},
crossref={LICS5},
pages={190--196}
}

@inproceedings{GehlotG90,
author={Gehlot, Vijay and Gunter, Carl},
title={Normal Process Representatives},
crossref={LICS5},
pages={200--207}
}

@inproceedings{BrownG90,
author={Brown, Carolyn and Gurr, Doug},
title={A Categorical Linear Framework for {P}etri Nets},
crossref={LICS5},
pages={208--218}
}

@inproceedings{Cerrito90,
author={Cerrito, Serenella},
title={A Linear Semantics for Allowed Logic Programs},
crossref={LICS5},
pages={219--227}
}

@inproceedings{SekarR90,
author={Sekar, R. C. and Ramakrishnan, I. V.},
title={Programming in Equantional Logic: Beyond Strong Sequentiality},
crossref={LICS5},
pages={230--241}
}

@inproceedings{DauchetT90,
author={Dauchet, M. and Tison, S.},
title={The Theory of Ground Rewrite Systems is Decidable},
crossref={LICS5},
pages={242--248}
}

@inproceedings{Lescanne90,
author={Lescanne, Pierre},
title={Well Rewrite Orderings},
crossref={LICS5},
pages={249--256},
abstract={This paper studies well (quasi) orderings described as
rewrite orderings and proposes a new family of well (quasi) orderings
that extends the embedding or divisibility order of G.~Higman.  For
instance, the well (quasi) orderings proposed in this paper may
contain pairs of the form $f(f(x)) > f(g(f(x)))$.  Conditions under
which the transitive closure of a well-founded rewrite relation is a
well-quasi-rodering are given.  Finally, an attempt to extend the
recursive path ordering is proposed.}
}

@inproceedings{MurthyR90,
author={Murthy, Chetan R. and Russell, James R.},
title={A Constructive Proof of {H}igman's Lemma},
crossref={LICS5},
pages={257--267}
}

@inproceedings{KirchnerK90,
author={Kirchner, Claude and Klay, Francis},
title={Syntactic Theories and Unification},
crossref={LICS5},
pages={270--277}
}

@inproceedings{Nipkow90,
author={Nipkow, Tobias},
title={Proof Transformations for Equational Theories},
crossref={LICS5},
pages={278--288}
}

@inproceedings{BoudetCD90,
author={Boudet, Alexandre and Contejean, Evelyne and Devie,
Herv{\'e}},
title={A New {$AC$} Unification Algorithm with an Algorithm for
Solving Systems of Diophantine Equations},
crossref={LICS5},
pages={289--299}
}

@inproceedings{DorreR90,
author={D{\"o}rre, Jochen and Rounds, William C.},
title={On Subsumption and Semiunification in Feature Algebras},
crossref={LICS5},
pages={300--310}
}

@InProceedings{CosmadakisMR90,
author={Stavros S. Cosmadakis and Albert R. Meyer and Jon G. Riecke},
title={Completeness for typed lazy inequalities},
crossref={LICS5},
pages={312--320},
abstract={
Familiar $\beta\eta$-equational reasoning on $\lambda$-terms in {\em
unsound\/} for proving observational congruences when termination of
the standard lazy interpreter is taken into account.  We develop a
complete logic, based upon sequents, for proving
termination-observational congruences between simply-typed terms
without constants.  We show that the theory, like that of
$\beta\eta$-reasoning in the ordinary typed $\lambda$-calculus, is
decidable.}
}

@inproceedings{WandW90,
author={Wand, Mitchell and Wang, Zheng-Yu},
title={Conditional Lambda-Theories and the Verification of Static
Properties of Programs},
crossref={LICS5},
pages={321--332}
}

@inproceedings{GuzmanH90,
author={Guzm{\'a}n, Juan C. and Hudak, Paul},
title={Single-Threaded Polymorphic Lambda Calculus},
crossref={LICS5},
pages={333--343}
}

@inproceedings{FreydMRS90,
author={Freyd, P. and Mulry, P. and Rosolini, G. and Scott, D.},
title={Extensional {PER}s},
crossref={LICS5},
pages={346--354},
comment={An extended version appeared in {\em Information and
Computation}, 98(2):211--227, June 1992.}
}

@inproceedings{AbadiP90,
author={Abadi, M. and Plotkin, G. D.},
title={A Per Model of Polymorphism and Recursive Types},
crossref={LICS5},
pages={355--365},
abstract={
A model of Reynolds' polymorphic lambda calculus is provided, which
also allows the recursive definition of elements and types. The
technique is to use a good class of partial equivalence relations over
a certain cpo.  This allows the combination of inverse-limits for
recursion and intersection for polymorphism.}
}

@inproceedings{Phoa90,
author={Phoa, Wesley},
title={Effective Domains and Intrinsic Structure},
crossref={LICS5},
pages={366--377},
comment={No abstract.}
}

@inproceedings{Lewis90,
author={Lewis, Harry R.},
title={A Logic of Concrete Time Intervals (Extended Abstract)},
crossref={LICS5},
pages={380--389}
}

@inproceedings{AlurH90,
author={Alur, Rajeev and Henzinger, Thomas A.},
title={Real-time Logics: Complexity and Expressiveness},
crossref={LICS5},
pages={390--401}
}

@inproceedings{HarelLP90,
author={Harel, Eyal and Lichtenstein, Orna and Pnueli, Amir},
title={Explicit Clock Temporal Logic},
crossref={LICS5},
pages={402--413}
}

@inproceedings{AlurCD90,
author={Alur, Rajeev and Courcoubetis, Costas and Dill, David},
title={Model-Checking for Real-Time Systems},
crossref={LICS5},
pages={414--425}
}

@inproceedings{BurchCMDH90,
author={Burch, J. R. and Clarke, E. M. and McMillan, K. L. and Dill,
D. L. and Hwang, L. J.},
title={Symbolic Model Checking: $10^{20}$ States and Beyond},
crossref={LICS5},
pages={428--439},
comment={An extended version appeared in {\em Information and
Computation}, 98(2):142--170, June 1992.}
}

@inproceedings{CleavelandS90,
author={Cleaveland, Rance and Steffen, Bernhard},
title={When is ``Partial'' Adequate?  {A} Logic-Based Proof Technique
Using Partial Specifications},
crossref={LICS5},
pages={440--449}
}

@inproceedings{GoldmanL90,
author={Goldman, Kenneth J. and Lynch, Nancy A.},
title={Modelling Shared State in a Shared Action Model},
crossref={LICS5},
pages={450--463}
}

@inproceedings{EmersonES90,
author={Emerson, E. Allen and Evangelist, Michael and Srinivasan,
Jai},
title={On the Limits of Efficient Temporal Decidability (Extended
Abstract)},
crossref={LICS5},
pages={464--475}
}

@inproceedings{HarelRV90,
author={Harel, David and Rosner, Roni and Vardi, Moshe},
title={On the Power of Bounded Concurrency~{III}: Reasoning About
Programs (Preliminary Report)},
crossref={LICS5},
pages={478--488}
}

@inproceedings{CroleP90,
author={Crole, Roy L. and Pitts, Andrew M.},
title={New Foundations for Fixpoint Computations},
crossref={LICS5},
pages={489--497},
comment={An extended versoin appeared as ``New foundations for
fixpoint computations: {FIX}-hyperdoctrines and the {FIX}-logic,''
{\em Information and Computation}, 98(2):171--210, June 1992.}
}

@inproceedings{Freyd90,
author={Freyd, Peter},
title={Recursive Types Reduced to Inductive Types},
crossref={LICS5},
pages={498--507}
}

                               6th LICS
                           July 15-18, 1991
                      Amsterdam, The Netherlands

@InProceedings{Leivant91,
author={Daniel Leivant},
title={A Foundational Delineation of Computational Feasiblity},
pages={2--11},
crossref={LICS6}
}

@InProceedings{AlessiB91,
author={Fabio Alessi and Franco Barbanera},
title={Towards a Semantics for the {QUEST} Language},
pages={12--21},
crossref={LICS6}
}

@InProceedings{Aczel91,
author={Peter Aczel},
title={Term Declaration Logic and Generalised Compsita},
pages={22--30},
crossref={LICS6}
}

@InProceedings{HodasM91,
author={Joshua S Hodas and Dale Miller},
title={Logic Programming in a Fragment of Intuitionistic Linear Logic},
pages={32--42},
crossref={LICS6}
}

@InProceedings{LaftontS91,
author={Y. Lafont and T. Streicher},
title={Games Semantics for Linear Logic},
pages={43--50},
crossref={LICS6}
}

@InProceedings{LincolnSS91,
author={Patrick Lincoln and Andre Scedrov and Natarajan Shankar},
title={Linearizing Intuitionistic Implication},
pages={51--62},
crossref={LICS6}
}

@InProceedings{MalacariaR91,
author={Pasquale Malacaria and Laurent Regnier},
title={Some Results on the Interpretation of $\lambda$-calculus in
Operator Algebras},
pages={63--72},
crossref={LICS6}
}

@InProceedings{Pfenning91,
author={Frank Pfenning},
title={Unification and Anti-Unification in the Calculus of Constructions},
pages={74--85},
crossref={LICS6}
}

@InProceedings{Audebaud91,
author={Philippe Audebaud},
title={Partial Objects in the Calculus of Constructions},
pages={86--95},
crossref={LICS6}
}

@InProceedings{Murthy91,
author={Chetan R. Murthy},
title={An Evaluation Semantics for Classical Proofs},
pages={96--107},
crossref={LICS6}
}

@InProceedings{CleavelandZ91,
author={Rance Cleaveland and Amy E. Zwarico},
title={A Theory of Testing for Real-Time},
pages={110--119},
crossref={LICS6}
}

@InProceedings{Hungar91,
author={Hardi Hungar},
title={Complexity Bounds of {Hoare}-style Proof Systems},
pages={120--126},
crossref={LICS6}
}

@InProceedings{HungZ91,
author={Hing-Kai Hung and Jeffery I. Zucker},
title={Semantics of Pointers, Referencing and Dereferencing with
Intensional Logic},
pages={127--136},
crossref={LICS6}
}

@InProceedings{BucciarelliE91,
author={Antonio Bucciarelli and Thomas Ehrhard},
title={Sequentiality and Strong Stability},
pages={138--145},
crossref={LICS6}
}

@InProceedings{Stoughton91,
author={Allen Stoughton},
title={Parallel {PCF} Has a Unique Extensional Model},
pages={146--151},
crossref={LICS6}
}

@InProceedings{Taylor91,
author={Paul Taylor},
title={The Fixed Point Property in Synthetic Domain Theory},
pages={152--160},
crossref={LICS6}
}

@InProceedings{Howe91,
author={Douglas J. Howe},
title={On Computational Open-Endedness in {Martin-L{\"o}f's} Type Theory},
pages={162--172},
crossref={LICS6}
}

@InProceedings{Mendler91,
author={Nax Paul Mendler},
title={Predicative Type Universes and Primitive Recursion},
pages={173--184},
crossref={LICS6}
}

@InProceedings{Statman91,
author={Rick Statman},
title={Freyd's Hierarchy of Combinator Monoids},
pages={186--190},
crossref={LICS6}
}

@InProceedings{Tronci91,
author={Enrico Tronci},
title={Equational Prgoramming in $\lambda$-calculus},
pages={191-202},
crossref={LICS6}
}

@InProceedings{BergerS91,
author={U. Berger and H. Schwichtenberg},
title={An Inverse of the Evaluation Functional for Typed $\lambda$-calculus},
pages={203--211},
crossref={LICS6}
}

@InProceedings{Kozen91,
author={Dexter Kozen},
title={A Completeness Theorem for {Kleene} Algebras and the Algebra of
Regular Events},
pages={214--225},
crossref={LICS6}
}

@InProceedings{AvronH91,
author={A. Avron and J. Hirshfeld},
title={On First Order Database Query Languages},
pages={226--231},
crossref={LICS6}
}

@InProceedings{PeledKP91,
author={Doron Peled and Shmuel Katz and Amir Pnueli},
title={Specifying and Proving Serializability in Temporal Logic},
pages={232--244},
crossref={LICS6}
}

@InProceedings{CamilleriW91,
author={Juanito Camilleri and Glynn Winskel},
title={{CCS} with Priority Choice},
pages={246--255},
crossref={LICS6}
}

@InProceedings{KlarlundK91,
author={Nils Klarlund and Dexter Kozen},
title={Rabin Measures and Their Applications to Fairness and Automata Theory},
pages={256--265},
crossref={LICS6}
}

@InProceedings{JonssonL91,
author={Bengt Jonsson and Kim Guldstrand Larsen},
title={Specification and Refinement of Probabilistic Processes},
pages={266--277},
crossref={LICS6}
}

@InProceedings{PacholskiS91,
author={Leszek Pacholski and Wies{\l}aw Szwast},
title={On the 0-1 Law for the class of Existential Second Order
Minimal {G{\"o}del} Sentences with Equality},
pages={280--285},
crossref={LICS6}
}

@InProceedings{BonetB91,
author={Maria Luisa Bonet and Samuel r. Buss},
title={On the Deduction Rule and the Number of Proof Lines},
pages={286--297},
crossref={LICS6}
}

@InProceedings{FruhwirthSVY91,
author={Thom Fr{\"u}hwirth and Ehud Shapiro and Mose Y. Vardi and Eyal
Yardeni},
title={Logic Programs as Types for Logic Programs},
pages={300--309},
crossref={LICS6}
}

@InProceedings{KiferW91,
author={Michael Kifer and James Wu},
title={A First-Order Theory of Types and Polymorphism in Logic Programming},
pages={310--321},
crossref={LICS6}
}

@InProceedings{CortesiFW91,
author={A. Cortesi and G. Fil{\'e} and W. Winsborough},
title={{\em Prop} revisited: Propositional Formula as Abstract Domain
for Groundness Analysis},
pages={322--327},
crossref={LICS6}
}

@InProceedings{Stuckey91,
author={Peter J. Stuckey},
title={Constructive Negation for Constraint Logic Programming},
pages={328--339},
crossref={LICS6}
}

@InProceedings{Nipkow91,
author={Tobias Nipkow},
title={Higher-Order Critical Pairs},
pages={342--349},
crossref={LICS6}
}

@InProceedings{JouannaudO91,
author={Jean-Pierre Jouannaud and Mitsuhiro Okada},
title={A Computation Model for Executable Higher-Order Algebraic
Specification Languages},
pages={350--361},
crossref={LICS6}
}

@InProceedings{Ryan91,
author={Mark Ryan},
title={Defaults and Revision in Structured Theories},
pages={362--373},
crossref={LICS6}
}

@InProceedings{HuttelS91,
author={Hans H{\"u}ttel and Colin Stirling},
title={Actions Speak Louder than Words: Proving Bisimilarity for
Context-Free Processes},
pages={376--386},
crossref={LICS6}
}

@InProceedings{Vaandrager91,
author={Frits W. Vaandrager},
title={On the Relationship Between Process Algebra and Input/Output
Automata},
pages={387--398},
crossref={LICS6}
}

@InProceedings{Boer91,
author={F. de Boer},
title={A Compositional Proof System for Dynamic Process Creation},
pages={399--405},
crossref={LICS6}
}

@InProceedings{GodefroidW91,
author={Patrice Godefroid and Pierre Wolper},
title={A Partial Approach to Model Checking},
pages={406--415},
crossref={LICS6}
}

                               7th LICS
                           June 22-25, 1992
                        Santa Cruz, California

@InProceedings{Dowek92,
title={Third Order Matching is Decidable},
author={Gilles Dowek},
pages={2--10},
crossref={LICS7},
abstract={The {\em higher order matching} problem is the problem of
determining whether a term is an instance of another in the simply
typed $\lambda$-calculus, i.e. to solve the equation $a = b$ where $a$
and $b$ are simply typed $\lambda$-terms and $b$ is ground. The
decidability of this problem is still open. We prove the decidability
of the particular case in which the variables occurring in the term
$a$ are at most third order.}
}

@InProceedings{KapurN92,
title={Double-exponential Complexity of Computing a Complete Set of
ac-unifiers},
author={Deepak Kapur and Paliath Narendran},
pages={11--21},
crossref={LICS7},
abstract={A new algorithm for computing a complete set of unifiers for
two terms involving associative-commutative function symbols is
presented.  The algorithm is based on a non-deterministic algorithm
given by the authors in 1986 to show the NP-completeness of
associative-commutative unifiability.  The algorithm is easy to
understand, its termination can be easily established.  More
importantly, its complexity can be easily analyzed and is shown to be
doubly exponential in the size of the input terms.  The analysis also
shows that there is a double-exponential upper bound on the size of a
complete set of unifiers of two input terms.  Since there is a family
of simple associative-commutative unification problems which have
complete sets of unifiers whose size is doubly exponential, the
algorithm is optimal in its order of complexity in this sense.  This
is the first associative-commutative unification algorithm whose
complexity has been completely analyzed.  The approach can also be
used to show a single exponential complexity for computing a complete
set of unifiers for terms involving associative-commutative function
symbols which also have the identity.  Furthermore, for unification in
the presence of associative-commutative-idempotent operators we get a
doubly exponential bound.}
}

@InProceedings{GroveHK92,
title={Random Worlds and Maximum Entropy},
author={Adam J. Grove and Joseph Y. Halpern and Daphne Kollar},
pages={22--33},
crossref={LICS7},
abstract={Given a knowledge base $\theta$ containing first-order and
statistical facts, we consider a principled method, called the {\em
random-worlds method}, for computing a degree of belief that some
$\phi$ holds given $\theta$.  If the domain has size $N$, then we can
consider all possible worlds with domain $\{1,\ldots, N\}$ that
satisfy $\theta$, and compute the fraction of them in which $\phi$ is
true. We define the degree of belief to be the asymptotic value of
this fraction as $N$ grows large.  We show that when the vocabulary
underlying $\phi$ and $\theta$ uses constants and unary predicates
only, we can in many cases use a {\em maximum entropy} computation to
compute the degree of belief.  Making precise exactly when we can use
a maximum entropy calculation turns out to be subtle.  We explore the
subtleties, and provide sufficient conditions that cover many of the
cases that occur in practice.}
}

@InProceedings{Schwarz92,
title={Minimal Model Semantics for Nonmonotonic Modal Logics},
author={Grigori Schwarz},
pages={34--43},
crossref={LICS7},
abstract={Nonmonotonic logical formalisms try to capture an important
property of commonsense reasoning: adding new facts (``axioms'') may
invalidate previously believed facts (``theorems''). One of the first
approaches to the problem, the modal approach, was originated by
D.McDermott and J.Doyle in 1980--1982. The lack of intuitively clear
semantics of nonmonotonic modal logics led to disregarding the
original McDermott and Doyle's approach. We provide intuitively clear
Kripke style semantics for nonmonotonic modal logic. The provided
semantics turns out to be a convenient tool for dealing with
nonmonotonic modal theories.  It also proposes a semantic solution to
a problem which attracts much attention in knowledge representation
research: what is the minimal knowledge set given axioms describing
initial knowledge of a rational agent?}
}

@InProceedings{KolaitisV92,
title={Fixpoint Logic vs.\ Infinitary Logic in Finite-Model Theory},
author={Phokion G. Kolaitis and Moshe Y. Vardi},
pages={46--57},
crossref={LICS7},
abstract={In recent years several extensions of first-order logic have
been investigated in the context of finite-model theory.  Fixpoint
logic and the infinitary logic~$L^\omega_{\infty\omega}$ with a finite
number of variables have turned out to be of particular importance.
The study of fixpoint logic generated interactions with both database
theory and complexity theory, while the infinitary
logic~$L^\omega_{\infty\omega}$ proved to be a useful tool for
analyzing the expressive power of fixpoint logic.  In addition to
being a proper extension of fixpoint logic, $L^\omega_{\infty\omega}$
enjoys a game-theoretic characterization and possesses interesting
structural properties, such as the 0-1 law.
\par
In this paper we pursue further the study of the relationship between
$L^\omega_{\infty\omega}$ and fixpoint logic.  We observe that
equivalence of two finite structures with respect
to~$L^\omega_{\infty\omega}$ is expressible in fixpoint logic.  As a
first application of this, we obtain a normal-form theorem
for~$L^\omega_{\infty\omega}$ on finite structures.  We then focus on
the relative expressive power of first-order logic, fixpoint logic,
and $L^\omega_{\infty\omega}$ on arbitrary classes of finite
structures.  Our second main result characterizes when
$L^\omega_{\infty\omega}$ collapses to first-order logic on an
arbitrary class of finite structures.  This resolves affirmatively a
conjecture of G. L. McColm.}
}

@InProceedings{GraedelM92,
title={Deterministic vs.\ Nondeterministic Transitive Closure Logic},
author={Erich Gr{\"a}del and Gregory L. McColm},
pages={58--63},
crossref={LICS7},
abstract={We show that transitive closure logic (FO + TC) is strictly
more powerful than deterministic transitive closure logic (FO + DTC).
In fact, on certain classes of graphs, such as hypercubes or regular
graphs of large degree and girth, every query in (FO + DTC) is first
order expressible.  On the other hand, there are simple TC queries on
these classes that cannot be defined by first order formulae.}
}

@InProceedings{Stolboushkin92,
title={Axiomatizable Classes of Finite Models and Definability of
Linear Order},
author={Alex Stolboushkin},
pages={64--70},
crossref={LICS7},
abstract={It may happen that a first order formula with two free
variables over a signature defines a linear order on some finite
structure of the signature. Then, naturally, this finite structure is
rigid, i.e., admits the single (trivial) automorphism.  Also, the
class of all the finite structures such that the formula defines a
linear order on any of them, is finitely axiomatizable in the class of
all finite structures (of the signature).
\par
In the paper we show that the inverse is not true, that is, that there
exists a finitely axiomatizable class of rigid finite structures, such
that no first order formula defines a linear order on all the
structures of the class.
\par
To illustrate possible applications of the result in Finite Model
Theory, we show that Yu.~Gurevich's result that Beth's definability
theorem fails for finite models is an immediate corollary of the
result of the paper.}
}

@InProceedings{GonthierLM92,
title={An abstract standardisation theorem},
author={Georges Gonthier and Jean-Jacques L{\'e}vy and Paul-Andr{\'e}
Melli{\`e}s},
pages={72--81},
crossref={LICS7},
abstract={The standardisation theorem is a key theorem in the
$\lambda$-calculus.  It implies that any normal form can be reached by
the normal order (leftmost outermost) strategy.  The theorem states
that any reduction may be rearranged in top-down form and
left-to-right order.  This also holds in orthogonal term rewriting
systems (TRS), although the left-to-right order is more subtle.  We
give a new presentation of the standardisation property by means of
four axioms about the residual and nesting relations on redexes.  This
axiomatic approach provides a better understanding of standardisation,
and makes it applicable in other settings, such as dags or interaction
networks.  We also treat conflicts between redexes (critical pairs in
TRS).  The axioms include Berry's stability, proving it to be a
intrinsic notion of {\em deterministic\/} calculi.}
}

@InProceedings{Nakano92,
title={A Constructive Formalization of the Catch and Throw Mechanism},
author={Hiroshi Nakano},
pages={82--89},
crossref={LICS7},
abstract={The catch/throw mechanism is a programming construct for
non-local exit.  In the practical programming, this mechanism plays an
important role when programmers handle exceptional situations.  In
this paper we give a constructive formalization which captures the
mechanism in the proofs-as-programs notion.  We introduce a modified
version of LJ equipped with inference rules corresponding to the
operations of {\rm catch} and {\rm throw}.  Then we show that we can
actually extract programs which make use of the catch/throw mechanism
from proofs under a certain realizability interpretation.  Although
the catch/throw mechanism provides only a restricted access to the
current continuation, the formulation remains constructive in contrast
to the works due to Griffin and Murthy on more powerful facilities
such as {\em call/cc}
(call-{\penalty0}with-{\penalty0}current-{\penalty0}continuation) of
Scheme.}
}

@InProceedings{Murthy92,
title={A Computational Analysis of {Girard's} Translation and {LC}},
author={Chetan R. Murthy},
pages={90--101},
crossref={LICS7},
abstract={We explain Girard's new translation from classical to
constructive logic.  We give a compatible continuation-passing-style
(CPS) translation, and convert it to a C-rewriting machine evaluator
for control-operator programs, in the manner of Felleisen \& Friedman,
and a set of reduction/computation rules sufficient to represent the
evaluator.  We find that we must add one reduction rule to Felleisen's
calculus (evaluation under $\lambda$-abstraction).  This reduction
rule arises from a modified call-by-name CPS-translation.  We then
turn to Girard's new classical logic LC, and provide an intuitionistic
term-extraction procedure for this calculus, producing CPS functional
programs.  Using the syntactic properties of this language, we are
able to give simple proofs for the evidence properties of LC.  This
work sheds light on the design space of CPS-translations, and extends
the relation between control-operator languages and classical logic.}
}

@InProceedings{Sangiorgi92,
title={The Lazy Lambda Calculus in a Concurrency Scenario (Extended
Abstract)},
author={Davide Sangiorgi},
pages={102--109},
crossref={LICS7},
abstract={The use of lambda calculus in richer settings, possibly
involving parallelism, is examined in terms of its effect on the
equivalence between lambda terms.  We concentrate here on Abramsky's
lazy lambda calculus and we follow two directions.  First, the lambda
calculus is studied within a process calculus by examining the
equivalence $\stackrel\sim\leftrightarrow$ induced by Milner's
encoding into the $\pi$-calculus. We give exact operational and
denotational characterizations for $\stackrel\sim\leftrightarrow$.
Secondly, we examine Abramsky's applicative bisimulation when the
lambda calculus is augmented with (well-formed) operators, i.e.
symbols equipped with reduction rules describing their behaviour.
Then, maximal discrimination is obtained when all operators are
considered; we show that this discrimination coincides with the one
given by $\stackrel\sim\leftrightarrow$ and that the adoption of
certain non-deterministic operators is sufficient and necessary to
induce it.}
}

@InProceedings{Wing92,
title={Specification in Software Development},
author={Jeannette M. Wing},
pages={112},
crossref={LICS7},
abstract={My tutorial presents through examples various kinds of
specifications used during software development.  It focuses on the
practical aspects of the nature and use of formal specifications.  I
mention some open research problems that should be of particular
interest to the LICS community.}
}

@InProceedings{AcetoBV92,
title={Turning {SOS} Rules into Equations},
author={Luca Aceto and Bard Bloom and Frits Vaandrager},
pages={113--124},
crossref={LICS7},
abstract={Many process algebras are defined by structural operational
semantics (SOS).  Indeed, most such definitions are nicely structured
and fit the GSOS format of Bloom, Istrail and Meyer.  We give a
procedure for converting any GSOS language definition to a finite
complete equational axiom system (possibly with one infinitary
induction principle) which precisely characterizes strong bisimulation
of processes.}
}

@InProceedings{Stark92,
title={A Calculus of Dataflow Networks (Extended Abstract)},
author={Eugene W. Stark},
pages={125--136},
crossref={LICS7},
abstract={Dataflow networks are a paradigm for concurrent computation
in which a collection of concurrently and asynchronously executing
processes communicate by sending data values over FIFO communication
channels.  In this paper, we define a CCS-style calculus of dataflow
networks with a standard structural operational semantics.  A version
of weak bisimulation equivalence, called ``buffer bisimilarity,'' is
defined for this calculus, and its equational theory is investigated.
The main result is a completeness theorem for proving equations valid
under buffer bisimilarity.  The axioms have a familiar,
category-theoretic flavor, in which a dataflow process with $m$ input
ports and $n$ output ports is represented by an arrow from $m$ to $n$
in a category whose objects are the finite ordinals.}
}

@InProceedings{BoerKP92,
title={Asynchronous Communication in Process Algebra},
author={F. S. de Boer and J. W. Klop and C. Palamidessi},
pages={137--147},
crossref={LICS7},
abstract={We study the paradigm of asynchronous process communication,
as contrasted with the synchronous communication mechanism which is
present in process algebra frameworks such as CCS, CSP and ACP.  We
investigate semantics and axiomatizations with respect to various
observability criteria: bisimulation, traces and abstract traces. Our
aim is to develop a process theory which can be regarded as a kernel
for languages based on asynchronous communication, like data flow,
concurrent logic languages and concurrent constraint programming.}
}

@InProceedings{Ulidowski92,
title={Equivalences on Observable Processes},
author={Irek Ulidowski},
pages={148--159},
crossref={LICS7},
abstract={The aim of this paper is to find the finest `observable' and
`implementable' equivalence on concurrent processes.  This is a part
of a larger programme to develop a theory of observable processes
where semantics of processes are based on locally and finitely {\em
observable\/} process behaviour, and all process constructs are
allowed, provided their operational meaning is defined by
realistically {\em implementable\/} transition rules.
\par
Process behaviour which can be established by so-called local testing
but not global testing is called locally and finitely observable. We
define {\em copy+refusal\/} testing equivalence as
indistinguishability by copy+refusal tests consisting of {\em traces,
refusals\/} and {\em copying\/}, all of which are local.  It is argued
that copy+refusal tests are sufficient for local testing---adding any
other local tests to copy+refusal tests does not increase their
testing power.  Hence, copy+refusal equivalence is the finest
observable equivalence.
\par
By examining the structure of transition rules we propose several
conditions which all realistically implementable rules should satisfy.
Using these conditions, we define the ISOS format of rules. We show
that the ISOS contexts capture exactly the observable behaviour of
processes---ISOS trace congruence is proved to coincide with
copy+refusal equivalence. Hence, copy+refusal equivalence is also the
finest implementable equivalence.}
}

@InProceedings{TalpinJ92,
title={The Type and Effect Discipline},
author={Jean-Pierre Talpin and Pierre Jouvelot},
pages={162--173},
crossref={LICS7},
abstract={The {\em type and effect discipline} is a new framework for
reconstructing the principal type and the minimal effect of
expressions in implicitly typed polymorphic functional languages that
support imperative constructs.  The type and effect discipline
outperforms other polymorphic type systems.  Just as types abstract
collections of concrete values, {\em effects} denote imperative
operations on regions.  {\em Regions} abstract sets of possibly
aliased memory locations.
\par
Effects are used to control type generalization in the presence of
imperative constructs while regions delimit observable side-effects.
The observable effects of an expression range over the regions that
are free in its type environment and its type; effects related to
local data structures can be discarded during type reconstruction.
The type of an expression can be generalized with respect to the
variables that are not free in the type environment or in the
observable effect.}
}

@InProceedings{Jensen92,
title={Disjunctive Strictness Analysis},
author={Thomas P. Jensen},
pages={174--185},
crossref={LICS7},
abstract={This paper addresses the problem of constructing a
disjunctive strictness analysis for a higher--order, functional
language. We present a system of disjunctive types for strictness
analysis of typed $\lambda$--calculus and use the types to define a
program logic for strictness analysis. A disjunctive abstract
interpretation is then obtained as a sound and complete model of the
program logic. The results reported here extend earlier work on using
the tensor product of lattices to analyse disjunctive properties of
programs by abstract interpretation.}
}

@InProceedings{MasonT92,
title={References, Local Variables and Operational Reasoning},
author={Ian A. Mason and Carolyn L. Talcott},
pages={186--197},
crossref={LICS7},
abstract={In the well known paper~\cite{meyer-sieber-88popl} Meyer and
Sieber give a series of examples of programs that are operationally
equivalent (according to the intended semantics of block-structured
Algol-like programs) but which are not given equivalent denotations in
traditional denotational semantics.  Since numerous proof systems for
Algol are sound for the denotational models in
question,~\cite{meyer-et-al-1,meyer-et-al-2,sieber-85,olderog-83,manna-waldinger-81ai},
these equivalences, if expressible, must be independent of these
systems.
\par
In this paper we accomplish two goals. Firstly, we present the
first-order part of a new logic for reasoning about programs.
Secondly, we use this logic to prove the equivalence of the
Meyer-Sieber examples.  Our style of operational semantics naturally
provides for the symbolic evaluation of contexts. This allows us to
define the semantics of {\em contextual assertions}.  Contextual
assertions allows us to express that a property holds at the point in
the program text where the hole appears.  Contextual assertions
generalize Hoare's triples in that they can be nested, used as
assumptions, and their free variables may be quantified.  Our atomic
formulas express the (operational or observational) equivalence of
programs.  Neither Hoare's logic nor Dynamic logic incorporate this
ability, or make use of such equivalences (for example by replacing
one piece of program text by an equivalent one).  In this paper we
only describe the first order part of the logic.  The full logic, a
variable type theory of individuals and classes, is based on the
systems of Feferman~\cite{feferman-explicit-75,feferman-poly-90} and
Talcott~\cite{talcott-90disco} and is described in detail
in~\cite{mason-talcott-91modal}.}
}

@InProceedings{Kanovich92,
title={Horn Programming in Linear Logic Is {NP}-Complete},
author={Max I. Kanovich},
pages={200--210},
crossref={LICS7},
abstract={The question at issue is to develop a computational
interpretation of Girard's linear logic and to obtain efficient
decision algorithms for this logic, based on {\bf the bottom-up
approach}.  It involves starting with the simplest natural fragment of
linear logic and then expanding it step-by-step.
\par
We consider {\bf the smallest natural Horn fragment} of Girard's
linear logic and prove that this fragment is NP-complete.  As a
corollary, we obtain {\bf the affirmative solution for the problem
from} [P.Lincoln, J.Mitchell, A.Scedrov, and N.Shancar.  Decision
Problems for Propositional Linear Logic.  SRI-CSL-90-08, August,
1990]: {\em whether the multiplicative fragment of Girard's linear
logic is NP-complete}.
\par
Then we give a {\bf complete computational interpretation} for Horn
fragments enriched by the two {\em additive connectives\/}: $\oplus$
and $\&$, and by the {\em storage operator~!}.  Within the framework
of this interpretation, it becomes possible to explicitly formalize
and clarify the computational aspects of the fragments of linear logic
in question and establish {\bf exactly} the complexity level of these
fragments.}
}

@InProceedings{AbramskyJ92,
title={New Foundations for the Geometry of Interaction},
author={Samson Abramsky and Radha Jagadeesan},
pages={211-222},
crossref={LICS7},
abstract={Girard has proposed the programme of Geometry of
Interaction, which aims to to find a new middle ground between
denotational and operational semantics, capturing the essential
features of computational dynamics in a syntax-free fashion using
denotational tools.  He has implemented this programme using the
formalism of C*-algebras.
\par
In this paper, we present a new formal embodiment of Girard's
programme, with the following salient features:
\par
1. Our formalisation is based on Domain Theory, rather than
C*-algebras.  We replace Girard's ``execution formula'' by a least
fixpoint, essentially a generalisation of Kahn's semantics for
feedback in dataflow networks.  Coupled with the use of the other
distinctive construct of Domain theory, the lifting monad, this
enables us to interpret the whole of Classical Linear Logic, and to
prove soundness in full generality, thus addressing the technical
limitations of Girard's formalisation.
\par
2. We give a concrete computational interpretation of the Geometry of
Interaction in terms of dataflow networks.
\par
3. We show how the interpretation arises from the construction of a
categorical model of Linear Logic, and identify exactly what structure
is required of the ambient category in order to carry out the
interpretation.  This makes the definition of the interpretation much
more transparent.}
}

@InProceedings{GonthierAL92,
title={Linear Logic Without Boxes},
author={Georges Gonthier and Mart{\'\i}n Abadi and Jean-Jacques
L{\'e}vy},
pages={223--234},
crossref={LICS7},
abstract={Girard's original definition of proof nets for linear logic
involves boxes. The box is the unit for erasing and duplicating
fragments of proof nets. It imposes synchronization, limits sharing,
and impedes a completely local view of computation. Here we describe
an implementation of proof nets without boxes.  Proof nets are
translated into graphs of the sort used in optimal $\lambda$-calculus
implementations; computation is performed by simple graph rewriting.
This graph implementation helps in understanding optimal reductions in
the $\lambda$-calculus and in the various programming languages
inspired by linear logic.}
}

@InProceedings{LincolnM92,
title={Operational aspects of linear lambda calculus},
author={Patrick Lincoln and John Mitchell},
pages={235--246},
crossref={LICS7},
abstract={Linear logic is a resource-aware logic that is based on an
analysis of the classical proof rules of contraction (copying) and
weakening (throwing away).  Several previous researchers have studied
functional programming languages derived from linear logic according
to the ``formulas-as-types'' correspondence.  In languages with linear
logic types, one may hope that traditional implementation problems in
functional languages such as update in place could be simplified by
careful use of the type system.  In this paper, we prove that the
standard sequent calculus proof system of linear logic is equivalent
to a natural deduction style proof system.  Using the natural
deduction system, we investigate the pragmatic problems of type
inference and type safety for a linear lambda calculus.  Although
terms do not have a single most-general type (for either the standard
sequent presentation or our natural deduction formulation), there is a
set of most-general types that may be computed using unification.  The
natural deduction system also facilitates the proof that the type of
an expression is preserved by any evaluation step.  We also describe
an execution model and implementation, using a variant of the
``three-instruction machine'' ({\sc tim}).  A novel feature of the
implementation is that we distinguish garbage-collected ``non-linear''
memory from ``linear'' memory, which does not require garbage
collection and where it is possible to do secure update in place.}
}

@InProceedings{Pratt92,
title={Origins of the Calculus of Binary Relations},
author={Vaughan Pratt},
pages={248--254},
crossref={LICS7},
abstract={The calculus of binary relations was introduced by De~Morgan
in 1860, and was subsequently greatly developed by Peirce and
Schr\"oder.  Half a century later Tarski, J\'onsson, Lyndon, and Monk
further developed the calculus from the perspective of modern model
theory.}
}

@InProceedings{ComonHJ92,
title={Decidable Problems in Shallow Equational Theories (Extended
Abstract)},
author={Hubert Comon and Marianne Haberstrau and Jean-Pierre
Jouannaud},
pages={255--265},
crossref={LICS7},
abstract={Ground equational theories are a well-studied subclass of
theories for which all interesting problems have been shown to be
decidable, e.g. the word problem by Nelsson and Oppen, the unification
problem by Kozen~[4], the disunification problem by Comon~[1]. A
fundamental tool for studying ground theories is Gallier's et al.
polynomial-time ground completion algorithm~[2].
\par
Even if ground theories are very important for practice, many
interesting problems do not fall into this category. On the other
hand, there are some axioms, such as commutativity, or more generally
Malcev's permutative axioms, for which all the above problems are also
decidable.  These axioms share the same pattern: their variables occur
at depth at most one. We call {\em shallow} an equational theory which
can be presented by finitely many such axioms.  In this paper, we show
that the above problems are decidable for the whole class of shallow
theories.
\par
Decision procedures for ground theories are uniform: they take for
argument a ground theory and an instance of the problem, and give the
answer as result. There are very few classes of theories that enjoy a
uniform unification or disunification procedure: theories presented by
a convergent set of rewrite rules, and Kirchner's {\em syntactic}
theories~[3].  Both techniques enumerate the solutions of a
unification or disunification problem, but do not terminate in
general. However, scrutinizing Kozen's and Comon's decidability
proofs, it appears that ground theories are indeed syntactic theories
for which Kirchner's and Comon's uniform procedures terminate.
\par
Generalizing these results to shallow theories is non-trivial. First,
we generalize Kirchner's syntactic theories by allowing collapsing
axioms.  Since we may not assume that cyclic equations do not have
solutions, we introduce the new key concept of a {\em cycle-syntactic}
theory, which plays for cycles a role similar to syntacticness for
non-cyclic equations. A last difficulty arises with Lassez's {\em
lemma of independence of disequations}~[5] which assumes that the
ground term algebra has finitely many congruence classes, a property
that we show is decidable for shallow theories.
\par
Shallow presentations are not syntactic in general, nor
cycle-syntactic.  The main technique used throughout this paper, which
generalizes Gallier's et al. ground completion algorithm, is the
computation by ordered completion techniques of conservative
extensions of the starting shallow presentation which are
respectively, ground convergent, syntactic and cycle-syntactic. In all
cases, the property that variables occur at depth at most one appears
to be crucial.
\par
Shallow theories thus emerge as a fundamental non-trivial,
union-closed subclass of equational theories for which all important
questions are decidable: the word problem is decidable, the finiteness
of the number of equivalence classes is decidable, unification is
finitary, and disunification is decidable hence the corresponding
quotient algebras are completely axiomatizable.
\section*{References}
\begin{enumerate}

\item
H.~Comon.  Complete axiomatizations of some quotient term algebras.
In {\em Proc. ICALP}, 1991.

\item
J.~Gallier, P.~Narendran, D.~Plaisted, S.~Raatz, and W.~Snyder.  An
algorithm for finding canonical sets of ground rewrite rules in
polynomial time.  {\em J.ACM}.

\item
C.~Kirchner.  Computing unification algorithms.  In {\em Proc. 1st
LICS, Cambridge, Mass.}, 1986.

\item
D.~Kozen.  Positive first order logic is {NP}-complete.  {\em IBM J.
of Res. DEvelopp.}, 25(4):327--332, 1981.

\item
J.-L. Lassez, M.~J. Maher, and K.~G. Marriot.  Unification revisited.
In {\em Proc. Workshop on Found. of Logic and Functional Programming,
Trento, LNCS 306}. {Sprin\-ger-Verlag}, Dec.  1986.
\end{enumerate}}
}


@InProceedings{Caucal92,
title={Monadic Theory of Term Rewritings},
author={Didier Caucal},
pages={266--273},
crossref={LICS7},
abstract={We consider the monadic second-order theory of term
rewritings.  We show that the monadic theory of the rewriting (or the
suffix rewriting) of a ground rewrite system is undecidable.
Furthermore the first-order theory is undecidable for the prefix
derivation according to a linear context-free grammar on linear terms.
Nevertheless we introduce a new notion on terms with variables: a term
is entire if each of its subterms either is a variable, or is without
variable or has the same variables as the term.  We show that the
monadic theory is decidable (respectively undecidable) for the prefix
rewriting according to a rewrite system on entire terms, with an axiom
(respectively without axiom).}
}

@InProceedings{Toyama92,
title={Strong Sequentiality of Left-Linear Overlapping Term Rewriting
Systems},
author={Yoshihito Toyama},
pages={274--284},
crossref={LICS7},
abstract={Huet and Levy showed that for every strongly sequential
orthogonal (i.e., left-linear and non-overlapping) term rewriting
system, index reduction strategy is normalizing. This paper extends
their result to ``overlapping'' term rewriting systems.  We show that
index reduction is normalizing for the class of strongly sequential
left-linear term rewriting systems in which every critical pair can be
joined with ``root balanced reductions''.  This class includes all
weakly orthogonal left-normal systems, for which leftmost-outermost
reduction strategy is normalizing.  For example, leftmost-outermost
reduction strategy is normalizing for combinatory logic CL with the
overlapping rules ``$\mathop{\rm pred} (\mathop{\rm succ} x) -> x$''
and ``$\mathop{\rm succ} (\mathop{\rm pred} x) -> x$''.}
}

@InProceedings{Seth92,
title={There is No Recursive Axiomatization for Feasible Functionals
of Type~2},
author={Anil Seth},
pages={286--295},
crossref={LICS7},
abstract={Feasible functionals of type~2 are the analogs of well known
type~1 polynomial time computable functions. Cook suggested the
following necessary conditions which a class of feasible functionals
must satisfy. (1)~It must contain the basic feasible functionals
(2)~All the type~1 functions constructed from this class of
functionals and poly time type~1 functions using lambda calculus
operations should be poly-time.  All the type~2 functionals so
constructed should be in oracle poly time. (3)~The class should be
closed under lambda abstraction and application.
\par
In this paper we show a class of type~2 functionals, $C_2$, which
satisfies Cook's conditions and cannot be expressed as lambda closure
of type~1 poly-time functions and any recursively enumerable set of
type~2 feasible functionals. Further, no class of total type~2
functionals containing this class is representable as lambda closure
of an r.e.\ set of type~2 total computable functionals and type~1
poly-time functions.  This is a significant advance in the current
knowledge in this area as previously known most general class of
type~2 functionals satisfying Cook's conditions can be represented as
lambda closure of type~1 poly-time functions and 2 type~2 functionals.
$C_2$ includes this class.  Our definition of~$C_2$ provides a clear
computational procedure for functionals of~$C_2$. Such a
characterization for any class more general than the basic feasible
functionals was not known before.  Using functionals of class~$C_2$
the notion of polynomial time reducibility between two arbitrary
type~1 functions can be introduced which is more general than
Mehlhorn's notion.}
}

@InProceedings{Clote92,
title={Cutting Planes and constant depth {Frege} proofs},
author={P. Clote},
pages={296--307},
crossref={LICS7},
abstract={The cutting planes refutation system for propositional logic
is an extension of resolution and is based on showing the
non-existence of solutions for families of integer linear
inequalities.  We define a modified system of cutting planes with
limited extension and show that this system can polynomially simulate
constant depth Frege proof systems. Our principal tool to establish
this result is an effective version of cut elimination for modified
cutting planes with limited extension. Thus, within a polynomial
factor, one can simulate classical propositional logic proofs using
modus ponens by refutation-style proofs, provided the formula depth is
bounded by a constant.  Since there are polynomial size cutting planes
proofs for many elementary combinatorial principles (pigeonhole
principle, Ramsey's theorem), we propose propositional versions of the
Paris-Harrington theorem, Kanamori-McAloon theorem, and variants as
possible candidates for combinatorial tautologies which may require
exponential size cutting planes and Frege proofs.}
}

@InProceedings{Tiuryn92,
title={Subtype Inequalities},
author={Jerzy Tiuryn},
pages={308--315},
crossref={LICS7},
abstract={In this paper we study the complexity of the satisfiability
problem for subtype inequalities in simple types. The naive algorithm
which solves this problem runs in non-deterministic exponential time
for every predefined poset of atomic subtypings. In this paper we show
that over certain finite posets of atomic subtypings the
satisfiability problem for subtype inequalities is PSPACE-hard. On the
other hand we prove that if the poset of atomic subtypings is a
disjoint union of lattices, then the satisfiability problem for
subtype inequalities is solvable in PTIME. This result covers the
important special case of the unification problem which can be
obtained when the atomic subtype relation is equality (in this case
the poset is a union of one-element lattices).}
}

@InProceedings{HeintzeJ92,
title={An Engine for Logic Program Analysis},
author={Nevin Heintze and Joxan Jaffar},
pages={318--328},
crossref={LICS7},
abstract={Most logic program analyzers employ a standard approach
based on abstract interpretation.  At the core of these is a generic
algorithm or ``engine'' which is parameterized by an abstract domain.
This standard engine is essentially a fixpoint computation over the
abstract semantic equations of a program.  This paper presents a new
engine which is based on unfolding of semantic equations.  A main
advantage of the unfolding engine is a uniform treatment of structural
information in a program.  In particular, reasoning about partially
instantiated structures, an area where traditional algorithms have
been weak, is greatly enhanced.  The main result of this paper shows
that our engine is uniformly more accurate than the standard engine in
the following sense: given an abstract domain, the output of our
engine, for any program, is more accurate than that of the standard
engine.}
}

@InProceedings{AikenW92,
title={Solving Systems of Set Constraints (Extended Abstract)},
author={Alexander Aiken and Edward L. Wimmers},
pages={329--340},
crossref={LICS7},
abstract={Systems of set constraints are a natural formalism for many
problems in program analysis.  Set constraints are also a
generalization of tree automata.  We present an algorithm for solving
systems of set constraints built from free variables, constructors,
and the set operations of intersection, union, and complement.
Furthermore, we show that all solutions of such systems can be
finitely represented.}
}

@InProceedings{Saraswat92,
title={The Category of Constraint Systems is {Cartesian}-Closed},
author={Vijay Saraswat},
pages={341--345},
crossref={LICS7},
abstract={The development of constraint programming has brought to the
forefront the notion of *constraint systems* as certain first-order
systems of partial information [ref].  Connections between such
systems and domain theory have seemed apparent for some time, but have
not yet been explored in depth.  The need for such a study becomes
unavoidable, however, when one considers the development of
higher-order constraint programming languages. To give semantics to
such languages, it becomes necessary to find mathematical structures
in which recursive ``domain equations'' involving constraint systems
can be solved.
\par
In this paper we give a general definition of constraint systems as
certain first-order systems of partial information, utilizing
Gentzen-style sequents.  Constraint systems can be regarded as
enriching the propositional Scott information systems with minimal
first-order structure: the notion of variables, existential
quantification and substitution.  We take as morphisms approximable
maps that are generic in all but finitely many variables.  We show
that the resulting structure forms a category (called ConstSys).
Furthermore, the structure of Scott information systems lifts smoothly
to the first-order setting --- we show that the category is
cartesian-closed, and other usual functors over Scott information
systems (lifting, sums, Smyth power-domain) are also definable and
recursive domain equations involving these functors can be solved.
This makes it possible to use this category to define the semantics of
higher-order, concurrent constraint programming languages.}
}

@InProceedings{VaananenK92,
title={Generalized Quantifiers and Pebble Games on Finite Structures},
author={Phokion G. Kolaitis and Jouko A. V{\"a}{\"a}n{\"a}nen},
pages={348--359},
crossref={LICS7},
abstract={First-order logic is known to have a severely limited
expressive power on finite structures.  As a result, several different
extensions have been investigated, including fragments of second-order
logic, fixpoint logic, and the infinitary
logic~$L^\omega_{\infty\omega}$ in which every formula has only a
finite number of variables.  Here, we study {\em generalized
quantitifiers\/} in the realm of finite structures and combine them
with the infinitary logic~$L^\omega_{\infty\omega}$ to obtain the
logics $L^\omega_{\infty\omega}({\bf Q})$, where ${\bf Q} = \{\,Q_i :
i \in I \,\}$ is a family of generalized quantifiers on finite
structures.  Using the logics~$L^\omega_{\infty\omega}({\bf Q})$, we
can express polynomial-time properties that are not definable
in~$L^\omega_{\infty\omega}$, such as ``there are at least $n/2$ $x$''
($n$ is the size of the universe), without going to second-order
logic.
\par
We show that equivalence of finite structures relative
to~$L^\omega_{\infty\omega}$ can be characterized in terms of certain
pebble games that are a variant of the {\em Ehrenfeucht-Fra{\"\i}ss\'e
games}.  We combine this game-theoretic characterization with
sophisticated combinatorial tools from Ramsey theory, such as Van der
Waerden's Theorem and Folkman's Theorem, in order to investigate the
scopes and limits of generalized quantifiers in finite model theory.
We obtain sharp lower bounds for expressibility in the
logics~$L^\omega_{\infty\omega}({\bf Q})$ and discover an intrinsic
difference between adding finitely many simple unary generalized
quantifiers to~$L^\omega_{\infty\omega}$ and adding infinitely many.}
}

@InProceedings{Hella92,
title={Logical Hierarchies in {PTIME}},
author={Lauri Hella},
pages={360--368},
crossref={LICS7},
abstract={A generalized quantifier is $n$-ary if it binds any finite
number of formulas, but at most $n$ variables in each formula.  We
prove that for each integer~$n$, there is a property of finite models
which is expressible in fixpoint logic, or even in DATALOG, but not in
the extension of first-order logic by any set of $n$-ary quantifiers.
It follows that no extension of first-order logic by a finite set of
quantifiers captures all DATALOG-definable properties.  Furthermore,
we prove that for each integer~$n$, there is a LOGSPACE-computable
property of finite models which is not definable in any extension of
fixpoint logic by $n$-ary quantifiers.  Hence, the expressive power of
LOGSPACE, and a fortiori, that of PTIME, cannot be captured by adding
to fixpoint logic any set of quantifiers of bounded arity.}
}

@InProceedings{HalpernK92,
title={Zero-One Laws for Modal Logic},
author={Joseph Y. Halpern and Bruce M. Kapron},
pages={369--380},
crossref={LICS7},
abstract={We show that a 0-1 law holds for propositional modal logic,
both for structure validity and frame validity.  In the case of
structure validity, the result follows easily from the well-known 0-1
law for first-order logic.  However, our proof gives considerably more
information.  It leads to an elegant axiomatization for almost-sure
structure validity, and sharper complexity bounds.  Since frame
validity can be reduced to a $\Pi_1^1$ formula, the 0-1 law for frame
validity helps delineate when 0-1 laws exist for second-order logics.}
}

@InProceedings{Klarlund92,
title={Progress Measures, Immediate Determinacy, and a Subset
Construction for Tree Automata},
author={Nils Klarlund},
pages={382--393},
crossref={LICS7},
abstract={Using the new concept of progress measure, we give a
simplified proof of Rabin's fundamental result that the languages
defined by tree automata are closed under complementation.
\par
To do this we show that for infinite games based on tree automata, the
{\em forgetful determinacy\/} property of Gurevich and Harrington can
be strengthened to an {\em immediate determinacy\/} property for the
player who is trying to win according to a Rabin acceptance condition.
Moreover, we show a graph theoretic duality theorem for such
acceptance conditions.  We also present a strengthened version of
Safra's determinization construction.  Together these results and the
determinacy of Borel games yield a straightforward method for
complementing tree automata.
\par
Our construction is almost optimal, i.e., the state space blow-up is
essentially exponential---thus roughly the same as for automata on
finite or infinite words.  To our knowledge, no prior constructions
have been better than double exponential.}
}

@InProceedings{HenzingerNSY92,
title={Symbolic Model Checking for Real-time Systems},
author={Thomas A. Henzinger and Xavier Nicollin and Joseph Sifakis and
Sergio Yovine},
pages={394--406},
crossref={LICS7},
abstract={We describe finite-state programs over real-numbered time in
a guarded-command language with real-valued clocks.  Model checking
answers the question which states of a real-time program satisfy a
branching-time specification (given in an extension of CTL with clock
variables).  We develop an algorithm that computes this set of states
symbolically as a fixpoint of a functional on state predicates,
without constructing the state space.
\par
For this purpose, we introduce a $\mu$-calculus on computation trees
over real-numbered time.  Unfortunately, many standard program
properties, such as response {\em for all nonZeno execution
sequences\/} (during which time diverges), cannot be characterized by
fixpoints: we show that the expressiveness of the timed $\mu$-calculus
is incomparable to the expressiveness of timed~CTL.  Fortunately, this
result does not impair the symbolic verification of ``implementable''
real-time programs --- those whose safety constraints are
machine-closed with respect to diverging time and whose fairness
constraints are restricted to finite upper bounds on clock values.
All timed CTL properties of such programs are shown to be computable
as finitely approximable fixpoints in a simple decidable theory.}
}

@InProceedings{PfenningH92,
title={Compiler Verification in {LF}},
author={John Hannan and Frank Pfenning},
pages={407--418},
crossref={LICS7},
abstract={We sketch a methodology for the verification of compiler
correctness based on the LF Logical Framework as realized within the
Elf programming language.  We have applied this technique to specify,
implement, and verify a compiler from a simple functional programming
language to a variant of the Categorical Abstract Machine (CAM).}
}

@InProceedings{Fribourg92,
title={Mixing List Recursion and Arithmetic},
author={Laurent Fribourg},
pages={419--429},
crossref={LICS7},
abstract={We consider in this paper a special class of predicates.
Every class predicate, say p, has one argument denoted y of type list.
All the other arguments are integers and form a vector denoted X.  The
predicates are primitive recursively defined over the structure of y,
and the auxiliary predicates are arithmetic relations over the integer
arguments.  When two atoms of this class, say p1(y,X1) and p2(y,X2),
share the same list argument y, it induces an implicit relation
between the integers of X1 and X2. We describe a method for generating
under certain conditions an arithmetic expression that characterizes
this relation. The method is useful for proving or synthesizing
inductive assertions about programs with arrays.}
}

@InProceedings{Curien92,
title={Observable Algorithms on Concrete Data Structures},
author={P.-L. Curien},
pages={432--443},
crossref={LICS7},
abstract={This paper is a contribution to the investigation of
sequentiality and full abstraction for sequential programming
languages.  Like previous works on full abstraction, it focuses on the
language PCF (simply typed $\lambda$-calculus + arithmetic +
recursion).
\par
We fit novel ideas of R. Cartwright and M. Felleisen (CF hereafter) on
observable sequentiality into the framework of concrete data
structures (Kahn-Plotkin) and sequential algorithms (Berry-Curien).
An extension of the category of sequential algorithms is shown to
provide an order-extensional model of PCF.  This is striking, since
sequential algorithms, even the extended ones considered here, called
observable algorithms, are defined as decision trees and have thus an
intensional nature.  The key to this ``miracle'' is the presence of
errors in the semantic domains.  The model of observable algorithms is
fully abstract for an extension of PCF.  This extension has errors
too, as well as a control operation {\em catch} as found in languages
like Scheme or Common Lisp.
\par
Our definitions are equivalent to those of CF, but are more abstract
(and simpler) and make the relation with the previous model of
sequential algorithms clear.  New results are the proof of cartesian
closure (CF do not define a category), and the proof of adequacy of
the model.}
}

@InProceedings{FreydRR92,
title={Functorial Parametricity},
author={P. J. Freyd and E. P. Robinson and G. Rosolini},
pages={444--452},
crossref={LICS7},
abstract={In this paper we consider the idea of treating a
parameterized type as an arbitrary functor from some parametrizing
category to a category of types, and giving elements semantics as
natural transformations.  We show that under reasonable hypotheses
this is only possible when the parametrizing category is a groupoid.
This suggests a semantics for a ``semi-parametric'' form of
polymorphism.  In the final section we discuss the interpretation of
this form of parametricity in a PER model, and show that it coincides
with the ostensibly stronger form derived from dinaturality.}
}

@InProceedings{Geuvers92,
title={The {Church-Rosser} Property for $\beta\eta$-reduction in Typed
$\lambda$-Calculi},
author={Herman Geuvers},
pages={453--460},
crossref={LICS7},
abstract={In this paper we investigate the Church-Rosser property (CR)
for Pure Type Systems with $\beta\eta$-reduction. For Pure Type
Systems with only $\beta$-reduction, CR on well typed terms follows
immediately from CR on the so called 'pseudoterms' and subject
reduction. For $\beta\eta$-reduction, CR on the set of pseudoterms is
just false, as was shown by [Nederpelt 1973].  Here we prove that CR
(for $\beta\eta$) on the well-typed terms {\em of a fixed type\/}
holds, which is the maximum we can expect in view of Nederpelts
counterexample. The proof is given for a large class of Pure Type
systems that contains e.g. LF (for which CR for $\beta\eta$ was proved
by [Salvesen 1989] and [Coquand 1991]), F, F$\omega$ and the Calculus
of Constructions.  In the proof, one key lemma (a very weak form of CR
for $\beta\eta$ on pseudoterms) takes a central position. It is
remarkable that in the proof of this key lemma the counterexample to
CR for $\beta\eta$ is essentially used.
\section*{References}

\begin{enumerate}

\item[{[Coquand 1991]}]
Th. Coquand, An algorithm for testing conversion in type theory.  In
Huet and Plotkin (eds.), {\em Logical Frameworks\/}, Cambridge Univ.
Press.

\item[{[Nederpelt 1973]}]
R. P. Nederpelt, Strong normalization in a typed lambda calculus with
lambda structured types.  Ph.D. thesis, Eindhoven Technological
University, The Netherlands.

\item[{[Salvesen 1989]}]
A. Salvesen, The Church-Rosser Theorem for LF with $\eta$ reduction.
Notes of a talk presented at the BRA-Logical Frameworks meeting,
Antibes 1990.

\end{enumerate}}
}

@InProceedings{LiguoroPS92,
title={Retracts in simply typed $\lambda\beta\eta$-calculus},
author={U. de'Liguoro and A. Piperno and R. Statman},
pages={461--469},
crossref={LICS7},
abstract={In this paper retractions existing in all models of simply
typed lambda-calculus are studied, relating them to other relations
among types as isomorphisms, surjections and injections. A formal
system to deduce the existence of such retractions is shown to be
sound and complete with respect to retractions definable by linear
lambda-terms, and results aiming to a system complete w.r.t. the
``provable retractions'' tout court are established.}
}

% CROSSREFERENCES
% These must remain at the end of this file.

@Proceedings{LICS1,
title={Proceedings, Symposium on Logic in Computer Science},
booktitle={Proceedings, Symposium on Logic in Computer Science},
year=1986,
month=jun # { 16--18},
address={Cambridge, Massachusetts},
organization={IEEE Computer Society},
crossrefonly=1,
comment={IEEE Computer Society Order Number 720; Library of Congress
Number 86-81090; IEEE Catalog Number 86CH2321-8; ISBN 0-8186-0720-3}
}

@Proceedings{LICS2,
title={Proceedings, Symposium on Logic in Computer Science},
booktitle={Proceedings, Symposium on Logic in Computer Science},
year=1987,
month=jun # { 22--25},
address={Ithaca, New York},
organization={The Computer Society of the IEEE},
crossrefonly=1,
comment={Computer Society Order Number 793; Library of Congress Number
87-45360; IEEE Catalog Number 87CH2464-6; ISBN 0-8186-0793-9; SAN
264-620X}
}

@Proceedings{LICS3,
title={Proceedings, Third Annual Symposium on Logic in Computer
Science},
booktitle={Proceedings, Third Annual Symposium on Logic in Computer
Science},
year=1988,
month=jul # { 5--8},
address={Edinburgh, Scotland},
organization={IEEE Computer Society},
crossrefonly=1,
comment={Computer Society Order Number 853; Library of Congress Number
88-45439; IEEE Catalog Number 88CH2608-8; ISBN 0-8186-0853-6}
}

@Proceedings{LICS4,
title={Proceedings, Fourth Annual Symposium on Logic in Computer
Science},
booktitle={Proceedings, Fourth Annual Symposium on Logic in Computer
Science},
year=1989,
month=jun # { 5--8},
address={Asilomar Conference Center, Pacific Grove, California},
organization={IEEE Computer Society Press},
crossrefonly=1,
comment={IEEE Computer Society Order Number 1954; Library of Congress
Number 89-83865; IEEE Catalog Number 89CH2753-2; ISBN 0-8186-1954-6;
SAN 264-620X}
}

@Proceedings{LICS5,
title={Proceedings, Fifth Annual IEEE Symposium on Logic in Computer
Science},
booktitle={Proceedings, Fifth Annual IEEE Symposium on Logic in
Computer Science},
year=1990,
month=jun # { 4--7},
address={Philadelphia, Pennsylvania},
organization={IEEE Computer Society Press},
crossrefonly=1,
comment={IEEE Computer Society Order Number 2073; Library of Congress
Number 89-641304; IEEE Catalog Number 90CH2897-7; ISBN 0-8186-2073-0;
SAN 264-620X}
}

@Proceedings{LICS6,
title={Proceedings, Sixth Annual IEEE Symposium on Logic in Computer
Science},
booktitle={Proceedings, Sixth Annual IEEE Symposium on Logic in
Computer Science},
year=1991,
month=jul # { 15--18},
address={Amsterdam, The Netherlands},
organization={IEEE Computer Society Press},
crossrefonly=1,
comment={IEEE Computer Society Order Number 2230; Library of Congress
Number 89-641304; IEEE Catalog Number 91CH3025-4; ISBN 0-8186-2230-X}
}

@Proceedings{LICS7,
title={Proceedings, Seventh Annual IEEE Symposium on Logic in Computer
Science},
booktitle={Proceedings, Seventh Annual IEEE Symposium on Logic in
Computer Science},
year=1992,
month=jun # { 22--25},
address={Santa Cruz, California},
organization={IEEE Computer Society Press},
crossrefonly=1,
comment={IEEE Computer Society Order Number 2735; Library of Congress
Number 91-78307; IEEE Catalog Number 92CH3127-8; ISBN 0-8186-2735-2}
}