*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)

- 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.

6 ×#logic

5 ×#equation

4 ×#on the

4 ×#polymorphism

4 ×#proving

3 ×#formal method

3 ×#semantics

3 ×#set

3 ×#source code

2 ×#algebra

5 ×#equation

4 ×#on the

4 ×#polymorphism

4 ×#proving

3 ×#formal method

3 ×#semantics

3 ×#set

3 ×#source code

2 ×#algebra