Proceedings of the First Symposium on Logic in Computer Science
LICS, 1986.

@proceedings{LICS-1986,
	address       = "Cambridge, Massachusetts, USA",
	isbn          = "0-8186-0720-3",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the First Symposium on Logic in Computer Science}",
	year          = 1986,
}

Contents (42 items)

6 ×#logic
6 ×#proving
6 ×#semantics
4 ×#verification
3 ×#algorithm
3 ×#automation
3 ×#calculus
3 ×#equation
3 ×#equivalence
3 ×#on the

LICS-1986-Robinson #functional #programming #reduction #relational

Merging Functional with Relational Programming in a Reduction Setting (JAR), p. 2.

LICS-1986-Csirmaz #correctness #finite

Program Correctness on Finite Fields (LC, BH), pp. 4–10.

LICS-1986-GermanCH #axiom

True Relative Completeness of an Axiom System for the Language L4 (Abridged) (SMG, EMC, JYH), pp. 11–25.

LICS-1986-JonssonMW #data flow #deduction #network #synthesis #towards

Towards Deductive Synthesis of Dataflow Networks (BJ, ZM, RJW), pp. 26–37.

LICS-1986-RoundsK #calculus #logic #representation

A Complete Logical Calculus for Record Structures Representing Linguistic Information (WCR, RTK), pp. 38–43.

LICS-1986-Meyer #hoare #logic #semantics

Floyd-Hoare Logic Defines Semantics: Preliminary Version (ARM), pp. 44–48.

LICS-1986-BeckmanGW #algebra #execution #logic programming #parallel #source code

An Algebraic Model of Parallel Execution of Logic Programs (LB, RG, AW), pp. 50–57.

LICS-1986-Brookes #concurrent #correctness #csp #proving #semantics

A Semantically Based Proof System for Partial Correctness and Deadlock in CSP (SDB), pp. 58–65.

LICS-1986-MonteiroP #concurrent #formal method

A Sheaf-Theoretic Model of Concurrency (LM, FCNP), pp. 66–76.

LICS-1986-BensonB #automaton #bisimulation

Strong Bisimulation of State Automata (DBB, OBS), pp. 77–81.

LICS-1986-Mohring #algorithm #calculus #development

Algorithm Development in the Calculus of Constructions (CM), pp. 84–91.

LICS-1986-Schlipf #how #question

How Uncomputable is General Circumscription? (JSS), pp. 92–95.

LICS-1986-Shultis #design #implementation

The Design and Implementations of Intuit (JS), pp. 96–104.

LICS-1986-Mason #equivalence #first-order #lisp #proving #source code

Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation (IAM), pp. 105–117.

LICS-1986-Nerode #research

A Logician Looks at Expert Systems: Areas for Mathematical Research (AN), p. 120.

LICS-1986-AmadioBL #equation #higher-order #λ-calculus

The Finitary Projection Model for Second Order λ Calculus and Solutions to Higher Order Domain Equations (RMA, KBB, GL), pp. 122–130.

LICS-1986-FelleisenFKD #continuation #reasoning

Reasoning with Continuations (MF, DPF, EEK, BFD), pp. 131–141.

LICS-1986-Gunter #axiom

The Largest First-Order-Axiomatizable Cartesian Closed Category of Domains (CAG), pp. 142–148.

LICS-1986-HalpernWW

Good Rewrite Strategies for FP (JYH, JHW, ELW), pp. 149–162.

LICS-1986-Plaisted #nondeterminism #recursion #semantics #source code #using

The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations (DAP), pp. 163–174.

LICS-1986-AbadiM

A Timely Resolution (MA, ZM), pp. 176–186.

LICS-1986-ChouK #geometry #on the #proving #theorem proving

On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.

LICS-1986-Despeyroux #proving #semantics

Proof of Translation in Natural Semantics (JD), pp. 193–205.

LICS-1986-Kirchner #algorithm #unification

Computing Unification Algorithms (CK), pp. 206–216.

LICS-1986-CoppoZ #logic #type inference

Type inference and logical relations (MC, MZ), pp. 218–226.

LICS-1986-Coquand #analysis

An Analysis of Girard’s Paradox (TC), pp. 227–236.

LICS-1986-KnoblockC #type system

Formalized Metareasoning in Type Theory (TBK, RLC), pp. 237–248.

LICS-1986-MendlerPC #infinity #type system

Infinite Objects in Type Theory (NPM, PP, RLC), pp. 249–255.

LICS-1986-Girard #semantics

Quantitative and Qualitative Semantics (JYG), p. 258.

LICS-1986-Browne #algorithm #automation #finite #logic #using #verification

An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic (MCB), pp. 260–266.

LICS-1986-EmersonL #calculus #model checking #performance #μ-calculus

Efficient Model Checking in Fragments of the Propositional μ-Calculus (EAE, CLL), pp. 267–278.

LICS-1986-HalpernS #logic

A Propositional Model Logic of Time Intervals (JYH, YS), pp. 279–292.

LICS-1986-MakowskyS #equivalence #higher-order #on the #semantics #standard #verification

On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems (JAM, IS), pp. 293–300.

LICS-1986-PerrinS #automaton #decidability #equivalence #integer #monad

Automata on the Integers, Recurrence Distinguishability, and the Equivalence and Decidability of Monadic Theories (DP, PES), pp. 301–304.

LICS-1986-RosnerP #logic

A Choppy Logic (RR, AP), pp. 306–313.

LICS-1986-Parikh #distributed

Levels of Knowledge in Distributed Computing (RP), pp. 314–321.

LICS-1986-PnueliZ #probability #verification

Probabilistic Verification by Tableaux (AP, LDZ), pp. 322–331.

LICS-1986-VardiW #approach #automation #verification

An Automata-Theoretic Approach to Automatic Program Verification (MYV, PW), pp. 332–344.

LICS-1986-BachmairDH #equation #order #proving

Orderings for Equational Proofs (LB, ND, JH), pp. 346–357.

LICS-1986-JouannaudK #automation #equation #induction #proving

Automatic Proofs by Induction in Equational Theories Without Constructors (JPJ, EK), pp. 358–366.

LICS-1986-KapurM #induction #reasoning #specification

Inductive Reasoning with Incomplete Specifications (DK, DRM), pp. 367–377.

LICS-1986-Statman #combinator #on the #problem

On Translating λ Terms into Combinators; The Basis Problem (RS), pp. 378–382.