Proceedings of the Fifth Annual Symposium on Logic in Computer Science
LICS, 1990.

@proceedings{LICS-1990,
	address       = "Philadelphia, Pennsylvania, USA",
	isbn          = "0-8186-2073-0",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the Fifth Annual Symposium on Logic in Computer Science}",
	year          = 1990,
}

Contents (45 items)

6 ×#logic
5 ×#equation
4 ×#on the
4 ×#polymorphism
4 ×#proving
3 ×#formal method
3 ×#semantics
3 ×#set
3 ×#source code
2 ×#algebra

LICS-1990-KfouryT #polymorphism #re-engineering #λ-calculus

Type Reconstruction in Finite-Rank Fragments of the Polymorphic λ-Calculus (AJK, JT), pp. 2–11.

LICS-1990-RobinsonR #call-by #morphism #polymorphism #set

Polymorphism, Set Theory, and Call-by-Value (ER, GR), pp. 12–18.

LICS-1990-DrosteG #formal method #programming language #semantics

Universal Domains in the Theory of Denotational Semantics of Programming Languages (MD, RG), pp. 19–34.

LICS-1990-Jung #classification

The Classification of Continuous Domains (AJ), pp. 35–40.

LICS-1990-HeintzeJ #constraints #set

A Decision Procedure for a Class of Set Constraints (NH, JJ), pp. 42–51.

LICS-1990-LassezM #calculus #constraints

A Constraint Sequent Calculus (JLL, KM), pp. 52–61.

LICS-1990-Comon #algebra #equation

Solving Inequations in Term Algebras (HC), pp. 62–69.

LICS-1990-Meyden #logic

The Dynamic Logic of Permission (RvdM), pp. 72–78.

LICS-1990-MarekNR #formal method

A Theory of Nonmonotonic Rule Systems (VWM, AN, JBR), pp. 79–94.

LICS-1990-AllenCHA #proving #semantics

The Semantics of Reflected Proof (SFA, RLC, DJH, WEA), pp. 95–105.

LICS-1990-LarsenX #equation #using

Equation Solving Using Modal Transition Systems (KGL, LX), pp. 108–117.

LICS-1990-GlabbeekSST #generative #modelling #probability #process

Reactive, Generative, and Stratified Models of Probabilistic Processes (RJvG, SAS, BS, CMNT), pp. 130–141.

LICS-1990-Moller #axiom #finite

The Nonexistence of Finite Axiomatisations for CCS Congruences (FM), pp. 142–153.

LICS-1990-KolaitisV #logic

0-1 Laws for Infinitary Logics (PGK, MYV), pp. 156–167.

LICS-1990-Kolaitis #ambiguity #finite

Implicit Definability on Finite Structures and Unambiguous Computations (PGK), pp. 168–180.

LICS-1990-Clote

ALOGTIME and a Conjecture of S. A. Cook (PC), pp. 181–189.

LICS-1990-Courcelle #graph #higher-order #monad #on the #set

On the Expression of Monadic Second-Order Graph Properties Without Quantifications Over Sets of Edges (BC), pp. 190–196.

LICS-1990-GehlotG #process

Normal Process Representatives (VG, CAG), pp. 200–207.

LICS-1990-BrownG #category theory #framework #linear #petri net

A Categorical Linear Framework for Petri Nets (CB, DG), pp. 208–218.

LICS-1990-Cerrito #linear #logic programming #semantics #source code

A Linear Semantics for Allowed Logic Programs (SC), pp. 219–227.

LICS-1990-SekarR #equation #logic #programming

Programming in Equational Logic: Beyond Strong Sequentiality (RCS, IVR), pp. 230–241.

LICS-1990-DauchetT #decidability #formal method #term rewriting

The Theory of Ground Rewrite Systems is Decidable (MD, ST), pp. 242–248.

LICS-1990-Lescanne #order

Well Rewrite Orderings (PL), pp. 249–256.

LICS-1990-MurthyR #proving

A Constructive Proof of Higman’s Lemma (CRM, JRR), pp. 257–267.

LICS-1990-KirchnerK #unification

Syntactic Theories and Unification (CK, FK), pp. 270–277.

LICS-1990-Nipkow #equation #proving

Proof Transformations for Equational Theories (TN), pp. 278–288.

LICS-1990-BoudetCD #algorithm #equation #unification

A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations (AB, EC, HD), pp. 289–299.

LICS-1990-DorreR #algebra #on the

On Subsumption and Semiunification in Feature Algebras (JD, WCR), pp. 300–310.

LICS-1990-CosmadakisMR #lazy evaluation

Completeness for typed lazy inequalities (SSC, ARM, JGR), pp. 312–320.

LICS-1990-WandW #source code #verification

Conditional λ-Theories and the Verification of Static Properties of Programs (MW, ZYW), pp. 321–332.

LICS-1990-GuzmanH #polymorphism #thread #λ-calculus

Single-Threaded Polymorphic λ Calculus (JCG, PH), pp. 333–343.

LICS-1990-FreydMRS

Extensional PERs (PJF, PM, GR, DSS), pp. 346–354.

LICS-1990-AbadiP #morphism #polymorphism #recursion

A Per Model of Polymorphism and Recursive Types (MA, GDP), pp. 355–365.

LICS-1990-Phoa #effectiveness

Effective Domains and Intrinsic Structure (WP), pp. 366–377.

LICS-1990-Lewis #logic

A Logic of Concrete Time Intervals (HRL), pp. 380–389.

LICS-1990-AlurH #complexity #logic #realtime

Real-time Logics: Complexity and Expressiveness (RA, TAH), pp. 390–401.

LICS-1990-HarelLP #logic

Explicit Clock Temporal Logic (EH, OL, AP), pp. 402–413.

LICS-1990-AlurCD #model checking #realtime

Model-Checking for Real-Time Systems (RA, CC, DLD), pp. 414–425.

LICS-1990-BurchCMDH #model checking

Symbolic Model Checking: 10^20 States and Beyond (JRB, EMC, KLM, DLD, LJH), pp. 428–439.

LICS-1990-CleavelandS #proving #specification #using

When is “Partial” Adequate? A Logic-Based Proof Technique Using Partial Specifications (RC, BS), pp. 440–449.

LICS-1990-GoldmanL #modelling

Modelling Shared State in a Shared Action Model (KJG, NAL), pp. 450–463.

LICS-1990-EmersonES #decidability #on the #performance

On the Limits of Efficient Temporal Decidability (EAE, ME, JS), pp. 464–475.

LICS-1990-HarelRV #bound #concurrent #on the #power of #reasoning #source code

On the Power of Bounded Concurrency~III: Reasoning About Programs (DH, RR, MYV), pp. 478–488.

LICS-1990-CroleP #fixpoint

New Foundations for Fixpoint Computations (RLC, AMP), pp. 489–497.

LICS-1990-Freyd #induction #recursion

Recursive Types Reduced to Inductive Types (PJF), pp. 498–507.