**Machado, Patricia D. L.**-
**Testing from Structured Algebraic Specifications: The Oracle Problem**

Patricia D. L. Machado

**MacQueen, David**-
**Standard ML**

Harper, MacQueen and Milner

*LFCS report ECS-LFCS-86-2*

**Unifying Exceptions with Constructors in Standard ML**

Milner, Tofte, MacQueen, Appel

*LFCS report ECS-LFCS-88-55*

**Mader, Angelika**-
**An effective tableau system for the linear time mu-calculus**

Julian Bradfield, Javier Esparza and Angelika Mader

*LFCS report ECS-LFCS-95-337*

**Maharaj, Savitri**-
**A Type-Theoretic Analysis of Modular Specifications**

Savitri Maharaj

*LFCS report ECS-LFCS-97-354*

**Mason, Ian A.**-
**Using Typed Lambda Calculus to Implement Formal Systems on a Machine**

Avron, Honsell and Mason

*LFCS report ECS-LFCS-87-31*

**Hoare's Logic in the LF**

I. Mason

*LFCS report ECS-LFCS-87-32*

**Verification of Programs that Destructively Manipulate Data**

I. Mason

*LFCS report ECS-LFCS-87-40*

**Workshop on General Logic - Edinburgh 1987**

Avron, Harper, Honsell, Mason and Plotkin

*LFCS report ECS-LFCS-88-52*

**Matthews, David C J**-
**A Distributed Concurrent Implementation of Standard ML**

D. Matthews

*LFCS report ECS-LFCS-91-174*

**Adaptive selection of protocols for strict coherency in distributed shared memory**

Thierry Le Sergent and David C J Matthews

*LFCS report ECS-LFCS-94-306*

**LEMMA Interface Definition**

David C J Matthews and Thierry Le Sergent

*LFCS report ECS-LFCS-95-316*

**LEMMA: A Distributed Shared Memory with Global and Local Garbage Collection**

David C J Matthews and Thierry Le Sergent

*LFCS report ECS-LFCS-95-325*

**Papers on Poly/ML**

David C J Matthews

*LFCS report ECS-LFCS-95-335*

**McAdam, Bruce J.**-
**The C-LEMMA Memory Interface on the Cray T3D**

Christopher D. Walton and Bruce J. McAdam

*LFCS report ECS-LFCS-97-362*

**That About Wraps it Up: Using FIX to Handle Errors Without Exceptions, and Other Programming Tricks**

Bruce J. McAdam

*LFCS report ECS-LFCS-97-375*

**On the Unification of Substitutions in Type-Inference**

Bruce J. McAdam

*LFCS report ECS-LFCS-98-384*

**Graphs for Recording Type Information**

Bruce J. McAdam

*LFCS report ECS-LFCS-99-415*

**Repairing Type Errors in Functional Programs**

Bruce James McAdam

**McBride, Conor**-
**Dependently Typed Functional Programs and their Proofs**

Conor McBride

**McKinna, James Hugh**-
**Deliverables: an approach to program development in the Calculus of Constructions**

Rod Burstall and James McKinna

*LFCS report ECS-LFCS-91-133*

**Deliverables: a categorical approach to program development in type theory**

Rod Burstall and James McKinna

*LFCS report ECS-LFCS-92-242*

**Deliverables: a categorical approach to program development in type theory**

James Hugh McKinna

*LFCS report ECS-LFCS-92-247 (also published as CST-96-92)*

**Candidates for Substitution**

Healfdene Goguen and James McKinna

*LFCS report ECS-LFCS-97-358*

**Some Lambda Calculus and Type Theory Formalized**

James McKinna and Robert Pollack

*LFCS report ECS-LFCS-97-359*

**Mendler, Michael**-
**Compositional Characterization of observable Program Properties**

B. Steffen, C.B. Jay, M. Mendler

*LFCS report ECS-LFCS-89-99*

**Newtonian Arbiters Cannot be Proven Correct**

Michael Mendler and Terry Stroup

*LFCS report ECS-LFCS-92-252*

**A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification**

Michael Mendler

*LFCS report ECS-LFCS-93-255 (also published as CST-97-93)*

**Formal Design of a Class of Computers**

Li-Guo Wang and Michael Mendler

*LFCS report ECS-LFCS-95-333*

**Abstraction of Hardware Construction**

Li-Guo Wang and Michael Mendler

*LFCS report ECS-LFCS-95-334*

**Menni, Matias**-
**Exact completions and toposes**

Matias Menni

**Miller, Dale**-
**Logic Programming in a Fragment of Intuitionistic Linear Logic; Extended Abstract**

D Miller and J Hodas

*LFCS report ECS-LFCS-91-158*

**A Logic Programming Language with Lambda-Abstraction, Function Variables and Simple Unification**

D Miller

*LFCS report ECS-LFCS-91-159*

**Unification of Simply Typed Lambda-Terms as Logic Programming**

D Miller

*LFCS report ECS-LFCS-91-160*

**Millington, M**-
**Theories of translation correctness for concurrent programming language**

M. Millington

*LFCS report ECS-LFCS-87-39 (also published as CST-46-87)*

**Milner, Robin**-
**Is Computing an Experimental Science**

R.Milner

*LFCS report ECS-LFCS-86-1***Standard ML**

Harper, MacQueen and Milner

*LFCS report ECS-LFCS-86-2*

**A Calculus of Communicating Systems**

R.Milner

*LFCS report ECS-LFCS-86-7*

**A Complete Axiomatisation for Observational Congruence of Finite-State Behaviours**

R.Milner

*LFCS report ECS-LFCS-86-8*

**A Complete Protocol Verification using Relativized Bisimulation**

K. Larsen and R. Milner

*LFCS report ECS-LFCS-86-13*

**A Type Discipline for Program Modules**

R.Harper, R.Milner and M.Tofte

*LFCS report ECS-LFCS-87-28*

**Changes to the Standard ML Core Language**

R. Milner

*LFCS report ECS-LFCS-87-33*

**The Semantics of Standard ML - Version 1**

Harper, Milner, Tofte

*LFCS report ECS-LFCS-87-36*

**Operational and Algebraic Semantics of Concurrent Processes**

R Milner

*LFCS report ECS-LFCS-88-46*

**Unifying Exceptions with Constructors in Standard ML**

Milner, Tofte, MacQueen, Appel

*LFCS report ECS-LFCS-88-55*

**The Definition of Standard ML - Version 2**

R Harper, R Milner and M Tofte

*LFCS report ECS-LFCS-88-62*

**Co-Induction in Relational Semantics**

R. Milner and M. Tofte

*LFCS report ECS-LFCS-88-65*

**The Definition of Standard ML - Version 3**

Harper, Milner and Tofte

*LFCS report ECS-LFCS-89-81*

**A Calculus of Mobile Processes Pt.1**

Milner, Parrow and Walker

*LFCS report ECS-LFCS-89-85*

**A Calculus of Mobile Processes Pt.2**

Milner, Parrow and Walker

*LFCS report ECS-LFCS-89-86*

**Modal Logics for Mobile Processes**

R. Milner, J. Parrow and D. Walker

*LFCS report ECS-LFCS-91-136*

**The Polyadic pi-Calculus: A Tutorial**

Robin Milner

*LFCS report ECS-LFCS-91-180*

**Action Structures**

Robin Milner

*LFCS report ECS-LFCS-92-249*

**Action Structures for the pi-Calculus**

Robin Milner

*LFCS report ECS-LFCS-93-264*

**Mitchell, John**-
**The Essence of ML**

R. Harper and J. Mitchell

*LFCS report ECS-LFCS-87-42*

**Higher-Order Modules and the Phase Distinction**

Harper, Moggi and Mitchell

*LFCS report ECS-LFCS-90-112*

**Mitchell, Kevin**-
**Concurrency in a Natural Semantics**

Kevin Mitchell

*LFCS report ECS-LFCS-94-311*

**Multiple Values in Standard ML**

Kevin Mitchell

*LFCS report ECS-LFCS-94-312*

**Mitrani, Isi**-
**A Manufacturing Production Line with Service Interruptions**

Nigel Thomas and Isi Mitrani

*LFCS report ECS-LFCS-98-388*

**Moggi, Eugenio**-
**The Partial Lambda-Calculus**

E. Moggi

*LFCS report ECS-LFCS-88-63 (also published as CST-53-88)*

**Computational Lambda-Calculus and Monads**

E. Moggi

*LFCS report ECS-LFCS-88-66*

**Higher-Order Modules and the Phase Distinction**

Harper, Moggi and Mitchell

*LFCS report ECS-LFCS-90-112*

**An Abstract View of Programming Languages**

E. Moggi

*LFCS report ECS-LFCS-90-113*

**Moller, Faron**-
**Axioms for Concurrency**

Faron Moller

*LFCS report ECS-LFCS-89-84 (also published as CST-59-88)*

**The Nonexistence of Finite Axiomatisations for CCS congruences**

Faron Moller

*LFCS report ECS-LFCS-89-97*

**A Temporal Calculus of Communicating Systems**

Faron Moller and Chris Tofts

*LFCS report ECS-LFCS-89-104*

**A Timed Calculus of Communicating Systems**

Liang Chen, Stuart Anderson and Faron Moller

*LFCS report ECS-LFCS-90-127*

**Relating Processes with Respect to Speed**

F. Moller and C. Tofts

*LFCS report ECS-LFCS-91-143*

**Verification of Parallel Systems via Decomposition**

J F Groote and F Moller

*LFCS report ECS-LFCS-92-193*

**Decomposability, Decidability and Axiomatisability for Bisimulation Equivalence on Basic Parallel Processes**

S Christensen, Y Hirshfield and F Moller

*LFCS report ECS-LFCS-92-244*

**The Mobility Workbench. A tool for the pi-Calculus**

Björn Victor and Faron Moller

*LFCS report ECS-LFCS-94-285*

**A polynomial algorithm for deciding bisimilarity of normed context-free processes**

Yoram Hirshfeld, Mark Jerrum and Faron Moller

*LFCS report ECS-LFCS-94-286*

**A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes**

Yoram Hirshfeld, Mark Jerrum and Faron Moller

*LFCS report ECS-LFCS-94-288*

**Molloy, Michael**-
**Generating and counting Hamilton cycles in random regular graphs**

Alan Frieze, Mark Jerrum, Michael Molloy, Robert Robinson and Nicholas Wormald

*LFCS report ECS-LFCS-94-313*

**Moreira, Alvaro Freitas**-
**A Type-Based Locality Analysis for a Functional Distributed Language**

Alvaro Freitas Moreira

**Morley, Matthew John**-
**Tactics for State Space Reduction on the Concurrency Workbench**

M.J. Morley

*LFCS report ECS-LFCS-90-109*

**Modelling British Rail's Interlocking Logic: Geographic Data Correctness**

M Morley

*LFCS report ECS-LFCS-91-186*

**Safety Assurance in Interlocking Design**

Matthew John Morley

*LFCS report ECS-LFCS-96-348*