University of Edinburgh. Laboratory for Foundations of Computer Science

165 published titles

Translating CTL* into the modal u-calculus

(Contributor)

1 edition

Program specification and data refinement in type theory

(Contributor)

1 edition

Deliverables : an approach to program development in the Calculus of Constructions

(Contributor)

1 edition

A systolizing compilation scheme

(Contributor)

1 edition

An n-categorical pasting theorem

(Contributor)

1 edition

The lazy lambda calculus in a concurrency scenario

(Contributor)

1 edition

Modelling British Rail's interlocking logic : geographic data correctness

(Contributor)

1 edition

An interleaving model for real-time systems

(Contributor)

1 edition

Decidability and completeness in real-time processes

(Contributor)

1 edition

Fixpoint and loop constructions as colimits

(Contributor)

1 edition

Modelling reduction in confluent categories

(Contributor)

1 edition

Modal logics for mobile processes

(Contributor)

1 edition

The formalization and analysis of a communications protocol

(Contributor)

1 edition

Extended ML : past, present and future

(Contributor)

1 edition

A kernel specification formalism with higher-order parameterisation

(Contributor)

1 edition

Long [beta] [eta] normal forms and confluence

(Contributor)

1 edition

An ideal model for an extended [lambda]-calculus with refinement

(Contributor)

1 edition

Task allocation in monomorphic ant species

(Contributor)

1 edition

Proof search in the [lambda pi]-calculus

(Contributor)

1 edition

Tail recursion via universal invariants

(Contributor)

1 edition

The systematic derivation of control signals for systolic arrays

(Contributor)

1 edition

An improved systolic array for string correction

(Contributor)

1 edition

Embedding a CHDDL in a proof system

(Contributor)

1 edition

The Edinburgh SML Library

(Contributor)

1 edition

A decision procedure revisited : notes on direct logic, linear logic and its implementation

(Contributor)

1 edition

The synthesis of control signals for one-dimensional systolic arrays

(Contributor)

1 edition

Modal and temporal logics

(Contributor)

1 edition

Logic programming in a fragment of intuitionistic linear logic : extended abstract

(Contributor)

1 edition

A logic programming language with lambda-abstraction, function variables, and simple unification

(Contributor)

1 edition

Unification of simply typed lambda-terms as logic programming

(Contributor)

1 edition

Proof nets for multiplicative and additive linear logic

(Contributor)

1 edition

A framework for defining logics

(Contributor)

1 edition

An analysis of a Monte Carlo algorithm for estimating the permanent

(Contributor)

1 edition

Classes of systolic y-tree automata and a comparison with systolic trellis automata

(Contributor)

1 edition

The uniform proof-theoretic foundation of linear logic programming (extended abstract)

(Contributor)

1 edition

A distributed concurrent implementation of Standard ML

(Contributor)

1 edition

A language for value-passing CCS

(Contributor)

1 edition

Recent developments in systolic design

(Contributor)

1 edition

Modularizing the specification of a small database system in Extended ML

(Contributor)

1 edition

A mildly exponential approximation algorithm for the permanent

(Contributor)

1 edition

Coherence in category theory and the Church-Rosser property

(Contributor)

1 edition

Improved bounds for mixing rates of Markov chains and multicommodity flow

(Contributor)

1 edition

Structuring specifications in-the-Large and in-the-Small : higher-order functions, dependent types and inheritance in SPECTRAL

(Contributor)

1 edition

Relating processes with respect to speed

(Contributor)

1 edition

Actions speak louder than words : proving bisimilarity for context-free processes

(Contributor)

1 edition

Undecidable equivalences for basic process algebra

(Contributor)

1 edition

Silence is golden : branching bisimilarity is decidable for context-free processes

(Contributor)

1 edition

A unifying theory of dependent types I

(Contributor)

1 edition

Computer assisted proof for mathematics : an introduction using the LEGO proof system

(Contributor)

1 edition

Tail recursion through universal invariants

(Contributor)

1 edition

A proposed categorical semantics for Pure ML

(Contributor)

1 edition

From term models to domains

(Contributor)

1 edition

Building domains from graph models

(Contributor)

1 edition

An introduction to fibrations, topos theory, the effective topos and modest sets

(Contributor)

1 edition

CTL* and ECTL* as fragments of the modal u-calculus

(Contributor)

1 edition

Process-algebraic interpretations of positive linear and relevant logics

(Contributor)

1 edition

Fixpoints of Büchi automata

(Contributor)

1 edition

Parsing in the SML Kit

(Contributor)

1 edition

Functional compilation from the Standard ML core language to lambda calculus

(Contributor)

1 edition

A sub-logarithmic communication algorithm for the completely connected optical communication parallel computer

(Contributor)

1 edition

Brewing strong normalization proofs with LEGO

(Contributor)

1 edition

Operational semantics based formal symbolic simulation

(Contributor)

1 edition

Inductive data types : well-ordering types revisited

(Contributor)

1 edition

LEGO proof development system : user's manual

(Contributor)

1 edition

Listing graphs that satisfy first order sentences

(Contributor)

1 edition

Unlimp uniqueness as a Leitmotiv for implementation

(Contributor)

1 edition

On resolution in fragments of classical linear logic (extended abstract)

(Contributor)

1 edition

Bisimulation equivalence is decidable for all context-free processes

(Contributor)

1 edition

Modal and temporal logics for processes

(Contributor)

1 edition

Toward formal development of programs from algebraic specifications : model-theoretic foundations

(Contributor)

1 edition

Toward formal development of programs from algebraic specifications : parameterisation revisited

(Contributor)

1 edition

Verification of parallel systems via decomposition

(Contributor)

1 edition

Formal program development in modular prolog : a case study

(Contributor)

1 edition

Loop parallelization and unimodularity

(Contributor)

1 edition

A proof assistant for symbolic model-checking

(Contributor)

1 edition

Approximating the permanent : a simple approach

(Contributor)

1 edition

Relational parametricity and local variables (preliminary report)

(Contributor)

1 edition

Semantics of local variables

(Contributor)

1 edition

Object-oriented programming without recursive types

(Contributor)

1 edition

Intersection types and bounded polymorphism

(Contributor)

1 edition

An abstract view of objects and subtyping (preliminary report)

(Contributor)

1 edition

A set-theoretic setting for structuring theories in proof development

(Contributor)

1 edition

A unifying theory of dependent types : the schematic approach

(Contributor)

1 edition

Miscellaneous design issues in the ML Kit

(Contributor)

1 edition

Formal development of functional programs in type theory : a case study

(Contributor)

1 edition

Polymorphic type checking by interpretation of code

(Contributor)

1 edition

Action structures

(Contributor)

1 edition

A semantics for static type inference

(Contributor)

1 edition

A case study in safety-critical design

(Contributor)

1 edition

Observational equivalence and compiler correctness

(Contributor)

1 edition

Correctness proofs of compilers and debuggers : an overview of an approach based on structural operational semantics

(Contributor)

1 edition

On the [pi]-calculus and linear logic

(Contributor)

1 edition

The virtues of eta-expansion

(Contributor)

1 edition

Hiding and behaviour : an institutional approach

(Contributor)

1 edition

Deliverables : a categorical approach to program development in type theory

(Contributor)

2 editions

Newtonian arbiters cannot be proven correct

(Contributor)

1 edition

Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes

(Contributor)

1 edition

Logic programming via proof-valued computations

(Contributor)

1 edition

A unification algorithm for the [lambda pi]-calculus

(Contributor)

1 edition

Equivalences between logics and their representing type theories

(Contributor)

1 edition

A synopsis on the identification of linear logic programming languages (extended abstract)

(Contributor)

1 edition

Undecidable equivalences for basic parallel processes

(Contributor)

1 edition

Multiple inheritance via intersection types

(Contributor)

1 edition

Literate programming : a review

(Contributor)

1 edition

Mistakes and ambiguities in the definition of Standard ML

(Contributor)

1 edition

Statically typed friendly functions via partially abstract types

(Contributor)

1 edition

Enrichment through variation

(Contributor)

1 edition

Simulated annealing for graph bisection

(Contributor)

1 edition

Approximately counting Hamilton cycles in dense graphs

(Contributor)

1 edition

Structure and behaviour in hardware verification

(Contributor)

1 edition

The formalisation of a hardware description language in a proof system : motivation and applications

(Contributor)

1 edition

Uniform sampling modulo a group of symmetries using Markov chain simulation

(Contributor)

1 edition

Errata and remarks

(Contributor)

1 edition

Action structures for the [pi]-calculus

(Contributor)

1 edition

Correctness of data representations in Algol-like languages

(Contributor)

1 edition

On the decidability of model checking for several [mu]-calculi and Petri nets

(Contributor)

1 edition

A theory of bisimulation for the [lambda]-calculus

(Contributor)

1 edition

Algebraic theories for name-passing calculi

(Contributor)

1 edition

Decidability questions for bisimilarity of Petri nets and some related problems

(Contributor)

1 edition

The mobility workbench : a tool for the [pi]-calculus

(Contributor)

1 edition

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

(Contributor)

1 edition

A polynomial algorithm for deciding bisimularity of normed context-free processes

(Contributor)

1 edition

Subtyping in F [omega,lambda] is decidable

(Contributor)

1 edition

A very simple algorithm for estimating the number of k-colourings of a low-degree graph

(Contributor)

1 edition

Interfaces and extended ML

(Contributor)

1 edition

First-class polymorphisms for ML

(Contributor)

1 edition

Why tricategories?

(Contributor)

1 edition

Applying process refinement to a safety-relevant system

(Contributor)

1 edition

Locality and non-interleaving semantics in calculi for mobile processes

(Contributor)

1 edition

Higher-order subtyping

(Contributor)

1 edition

Decidability of model checking for infinite-state concurrent systems

(Contributor)

1 edition

Improved approximation algorithms for MAX k-CUT and MAX BISECTION

(Contributor)

1 edition

On modal mu-calculus and Büchi tree automata

(Contributor)

1 edition

Deciding equivalences in simple Process Algebras

(Contributor)

1 edition

Trapping mutual exclusion in the box calculus

(Contributor)

1 edition

A fully abstract semantics for causality in the [pi]-calculus

(Contributor)

1 edition

On the bisimulation proof method

(Contributor)

1 edition

High undecidability of weak bisimilarity for petri nets

(Contributor)

1 edition

An old sub-quadratic algorithm for finding extremal sets

(Contributor)

1 edition

The definition of Extended ML

(Contributor)

1 edition

Positive subtyping

(Contributor)

1 edition

Generating and counting Hamilton cycles in random regular graphs

(Contributor)

1 edition

Balancing load under large and fast load changes in distributed computing systems : a case study

(Contributor)

1 edition

Multiple values in standard ML

(Contributor)

1 edition

Concurrency in a natural semantics

(Contributor)

1 edition

Supporting formal reasoning about standard ML

(Contributor)

1 edition

On computing the subset graph of a collection of sets

(Contributor)

1 edition

Adaptive selection of protocols for strict coherency in distributed shared memory

(Contributor)

1 edition

Congruences in commutative semigroups

(Contributor)

1 edition

The computational complexity of counting

(Contributor)

1 edition

Towards a domain theory for termination proofs

(Contributor)

1 edition

Axiomatising linear time mu-calculus

(Contributor)

1 edition

A quasi-polynomial-time algorithm for sampling words from a context-free language

(Contributor)

1 edition

Formal design of a class of computers

(Contributor)

1 edition

Papers on Poly/ML

(Contributor)

1 edition

Correct separate and selective closure conversion

(Contributor)

1 edition

LEMMA interface definition

(Contributor)

1 edition

LEMMA : a distributed shared memory with global and local garbage collection

(Contributor)

1 edition

Computational Pćlya theory

(Contributor)

1 edition

On behavioural abstraction and behavioural satisfaction in higher-order logic

(Contributor)

1 edition

Lax naturality through enrichment

(Contributor)

1 edition

First steps on the representation of domains (extended abstract)

(Contributor)

1 edition

An effective tableau system for the linear time mu-calculus

(Contributor)

1 edition

Abstraction of hardware construction

(Contributor)

1 edition

Proof and design

(Contributor)

1 edition