Proceedings of the Second Symposium on Logic in Computer Science
LICS, 1987.

@proceedings{LICS-1987,
	address       = "Ithaca, New York, USA",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the Second Symposium on Logic in Computer Science}",
	year          = 1987,
}

Contents (37 items)

7 ×#logic
5 ×#proving
4 ×#λ-calculus
3 ×#first-order
3 ×#framework
3 ×#modelling
3 ×#on the
3 ×#semantics
3 ×#source code
2 ×#concurrent

LICS-1987-Milner #fixpoint

Some Uses of Maximal Fixed Points (RM), p. 3.

LICS-1987-Breazu-TannenM #morphism #polymorphism

Polymorphism is conservative over simple types (VT, ARM), pp. 7–17.

LICS-1987-GoguenM #algebra #multi #order

Order-Sorted Algebra solves the Constructor-Selector, Multiple (JAG, JM), pp. 18–29.

LICS-1987-Mendler #constraints #higher-order #recursion #λ-calculus

Recursive Types and Type Constraints in Second-Order λ Calculus (NPM), pp. 30–36.

LICS-1987-Wand #type inference

Complete Type Inference for Simple Objects (MW), pp. 37–44.

LICS-1987-Abramsky #logic

Domain Theory in Logical Form (SA), pp. 47–53.

LICS-1987-HarelPSS #on the #semantics

On the Formal Semantics of Statecharts (DH, AP, JPS, RS), pp. 54–64.

LICS-1987-Seely #framework #modelling

Modelling Computations: A 2-Categorical Framework (RAGS), pp. 65–71.

LICS-1987-GaifmanP #concurrent #modelling #partial order

Partial Order Models of Concurrency and the Computation of Functions (HG, VRP), pp. 72–85.

LICS-1987-BidoitF #logic programming

Minimalism subsumes Default Logic and Circumscription in Stratified Logic Programming (NB, CF), pp. 89–97.

LICS-1987-MillerNS #proving

Hereditary Harrop Formulas and Uniform Proof Systems (DM, GN, AS), pp. 98–105.

LICS-1987-GaifmanMSV #database #decidability #logic programming #optimisation #problem #source code

Undecidable Optimization Problems for Database Logic Programs (HG, HGM, YS, MYV), pp. 106–115.

LICS-1987-Reynolds #algol

Conjunctive Types and Algol-like Languages (JCR), p. 119.

LICS-1987-Abadi #power of #proving

The Power of Temporal Proofs (MA), pp. 123–130.

LICS-1987-AlpernS #proving

Proving Boolean Combinations of Deterministic Properties (BA, FBS), pp. 131–137.

LICS-1987-SistlaG #process #reasoning

Reasoning with Many Processes (APS, SMG), pp. 138–152.

LICS-1987-SistlaZ #logic #on the

On the Eventuality Operator in Temporal Logic (APS, LDZ), pp. 153–166.

LICS-1987-Vardi #concurrent #framework #source code #verification

Verification of Concurrent Programs: The Automata-Theoretic Framework (MYV), pp. 167–176.

LICS-1987-Emden #first-order #functional #logic #programming #relational

First-order Predicate Logic as a Common Basis for Relational and Functional Programming (MHvE), p. 179.

LICS-1987-ConstableS #type system

Partial Objects In Constructive Type Theory (RLC, SFS), pp. 183–193.

LICS-1987-HarperHP #framework #logic

A Framework for Defining Logics (RH, FH, GDP), pp. 194–204.

LICS-1987-Howe #behaviour

The Computational Behaviour of Girard’s Paradox (DJH), pp. 205–214.

LICS-1987-Allen

A Non-Type-Theoretic Definition of Martin-Löf’s Types (SA), pp. 215–221.

LICS-1987-KfouryTU #functional #source code

The Hierarchy of Finitely Typed Functional Programs (AJK, JT, PU), pp. 225–235.

LICS-1987-ImmermanK #bound

Definability with Bounded Number of Bound Variables (NI, DK), pp. 236–244.

LICS-1987-Thomas #first-order #infinity #logic #on the

On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees (WT), pp. 245–256.

LICS-1987-HalpernW #abstraction

Full Abstraction and Expressive Completenes for FP (JYH, ELW), pp. 257–271.

LICS-1987-Shoham #approach #logic #semantics

A Semantical Approach to Nonmonotic Logics (YS), pp. 275–279.

LICS-1987-FaginH #communication

I’m OK if You’re OK: On the Notion of Trusting Communication (RF, JYH), pp. 280–292.

LICS-1987-Goerdt #hoare #imperative #logic

Hoare Logic for λ-Terms as Basis of Hoare Logic for Imperative Languages (AG), pp. 293–299.

LICS-1987-MitchellM #modelling #λ-calculus

Kripke-Style models for typed λ calculus (JCM, EM), pp. 303–314.

LICS-1987-FreydS #aspect-oriented #polymorphism #semantics #λ-calculus

Some Semantic Aspects of Polymorphic λ Calculus (PJF, AS), pp. 315–319.

LICS-1987-BohmT #λ-calculus

X-Separability and Left-Invertibility in λ-calculus (CB, ET), pp. 320–328.

LICS-1987-BachmairD #first-order #proving #theorem proving

Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.

LICS-1987-GallierRS #equation #proving #theorem proving #using

Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.

LICS-1987-KirchnerL #equation

Solving Disequations (CK, PL), pp. 347–352.

LICS-1987-DauchetTHL #confluence #decidability #term rewriting

Decidability of the Confluence of Ground Term Rewriting Systems (MD, ST, TH, PL), pp. 353–359.