[an error occurred while processing this directive]
An error occured whilst processing this directive
All LFCS reports
View this list backwards.
- 1986
-
- Is Computing an Experimental
Science, R.Milner
- Standard ML, Harper, MacQueen
and Milner
- Functor-Category Semantics of
Programming Languages and Logics, R. Tennent
- Context-Dependent Bisimulation
between Processes, K. Larsen
- Semantical Analysis of Specification
Logic, R.Tennent
- Quantification in Algol-like
Languages, R.Tennent
- A Calculus of Communicating
Systems, R.Milner
- A Complete Axiomatisation for
Observational Congruence of Finite-State Behaviours,
R.Milner
- Computing with Categories,
R.Burstall and D.Rydeheard
- A Study in the Foundations of
Programming Methodology: Specifications, Institutions, Charters and
Parchments, R.Burstall and J.Goguen
- Modules and Persistence in Standard
ML, R.Harper
- Research in Interactive Theorem
Proving at Edinburgh University, R.Burstall
- A Complete Protocol Verification
using Relativized Bisimulation, K. Larsen and R.
Milner
- Introduction to Standard ML,
R.Harper
- Formal Specification of ML
Programs, D.Sannella
- Extended ML: An
institution-independent framework for formal program
development, D.Sannella and A.Tarlecki
- Toward formal development of
programs from algebraic specifications: implementations
revisited, D.Sannella and A.Tarlecki
- Verifying a CSMA/CD-protocol with
CCS, J. Parrow
- Data Abstraction and the
Correctness of Modular Programming, O.Schoett
- Gentzenizing Schroeder-Heister's
Natural extension of natural deduction, A. Avron
- Some thoughts on algebraic
specification, D.Sannella and A.Tarlecki
- Introduction to a Calculus of
Communicating Systems, D. Walker
- 1987
-
- A Framework for Defining
Logics, R.Harper, F.Honsell and G.Plotkin
- Comparing Linear and Branching Time
Temporal Logics, C. Stirling
- Inductively Defined Functions in
Functional Programming Languages, R. Burstall
- Submodule Construction as Equation
Solving in CCS, J. Parrow
- The Semantics and Proof Theory of
Linear Logic, A. Avron
- A Type Discipline for Program
Modules, R.Harper, R.Milner and M.Tofte
- Bisimulation equivalence and
divergence in CCS, D. Walker
- Simple Consequence Relations,
A. Avron
- Using Typed Lambda Calculus to
Implement Formal Systems on a Machine, Avron, Honsell and
Mason
- Hoare's Logic in the LF, I.
Mason
- Changes to the Standard ML Core
Language, R. Milner
- An Environment for Formal
Systems, T G Griffin
- Synchronisation Flow Algebra,
J Parrow
- The Semantics of Standard ML -
Version 1, Harper, Milner, Tofte
- The Generation of Concurrent Code
for Declarative Languages, N. Rothwell
- A Categorical Programming
Language, T. Hagino
- Theories of translation correctness
for concurrent programming language, M. Millington
- Verification of Programs that
Destructively Manipulate Data, I. Mason
- Fifth Workshop on Specification of
Abstract Data Types, D. Sannella
- The Essence of ML, R. Harper
and J. Mitchell
- Relative Completeness in Algebraic
Specification, Lin Huimin
- 1988
-
- A Typed Lambda Calculus with
Categorical Type Constructors, T Hagino
- Analysing mutual exclusion
algorithms using CCS, D Walker
- Operational and Algebraic Semantics
of Concurrent Processes, R Milner
- Models of Self-Descriptive Set
Theories, F Honsell
- Foundations and Proof Theory of
3-valued Logics, A.Avron
- Temporal Ordering for
Concurrency, C. Tofts
- How to Breed
Compiler/Interpreters, A. Gordon
- Bisimulations for Concurrency,
I. Castellani
- Workshop on General Logic -
Edinburgh 1987, Avron, Harper, Honsell, Mason and
Plotkin
- On Functors Expressible in the
Polymorphic Typed Lambda Calculus, J. Reynolds and G.
Plotkin
- Operational Semantics and
Polymorphic Type Inference, Mads Tofte
- Unifying Exceptions with
Constructors in Standard ML, Milner, Tofte, MacQueen,
Appel
- A Survey of Formal Software
Development Methods, D. Sannella
- A Higher-order Calculus and Theory
Abstraction, Zhaohui Luo
- CC and its Meta Theory,
Zhaohui Luo
- Constructing Type Systems over an
Operational Semantics, R. Harper
- Some Fundamental Algebraic Tools
for the Semantics of Computation - Part III: Indexed
Categories, A Tarlecki, R M Burstall and J A Goguen
- The Interactive Proof Editor - An
Experiment in Interactive Theorem, B Ritchie and P
Taylor
- The Definition of Standard ML -
Version 2, R Harper, R Milner and M Tofte
- The Partial Lambda-Calculus,
E. Moggi
- E.U. Postgraduate Exam Questions in
Computation Theory, D. Sannella
- Co-Induction in Relational
Semantics, R. Milner and M. Tofte
- Computational Lambda-Calculus and
Monads, E. Moggi
- An Equational Formulation of
LF, R. Harper
- The Design and Implementation of an
Interactive Proof Editor, B. Ritchie
- A Natural Deduction treatment of
Operational Semantics, R Burstall and F. Honsell
- 1989
-
- Using Constructions as a
Metalanguage, Paul Taylor
- Towards formal development of ML
programs, foundations and methodology, Donald Sannella and
Andrzej Tarlecki
- Proving correctness of constructor
implementations, Jorge Farrés-Casals
- Four Lectures on Standard ML,
Mads Tofte
- THORN: A Theorem-Prover that
compiles first-order Logic into LISP, M. Tarver
- Structure and Representation in
LF, Harper, Sannella and Tarlecki
- Characteristic Formulae for CCS
with Divergence, B. Steffen
- Proof-Theoretic Characterisations
of Logic Programming, J. Andrews
- Local Model Checking in the Modal
Mu-Calculus, C. Stirling and D. Walker
- Finite Constants: Characterizations
of a new decidable set of constants, B. Steffen and J.
Knoop
- DIALOG: A Theorem-proving
environment designed to unify Functional and Logic Programming,
M. Tarver
- The Definition of Standard ML -
Version 3, Harper, Milner and Tofte
- Optimal Data Flow Analysis via
Observational Equivalence, Bernhard Steffen
- The Concurrency Workbench: A
Semantics-based Verification Tool for Finite-State Systems,
R. Cleaveland, J. Parrow and B. Steffen
- Axioms for Concurrency,
Faron Moller
- A Calculus of Mobile Processes
Pt.1, Milner, Parrow and Walker
- A Calculus of Mobile Processes
Pt.2, Milner, Parrow and Walker
- Relating Petri Nets to Formulae of
Linear Logic, Carolyn Brown
- On Natural deduction style
semantics, environments and stores, Christian-Emil
Ore
- Playing with Lego: Some examples of
developing mathematics in the Calculus of Constructions,
Paul Taylor
- Some Fundamental Algebraic Tools
for the Semantics of Computation. Part 3. Indexed Categories,
R. Burstall, J. Goguen and A. Tarlecki
- Automated Analysis of Mutual
Exclusion Algorithms using CCS, D J Walker
- The Structure of free closed
categories, C Barry Jay
- Equations, dependent equations and
quasi-dependent equations -- on their unification, Sun
Yong
- Equational Characterization of
Binding (Extended Abstract), Sun Yong
- Logical Design of VLSI Circuit with
Extension of Uncertainty (or monotonic functional completeness of
Kleene ternary logic), Sun Yong
- Petri Nets as Quantales,
Carolyn Brown
- The Nonexistence of Finite
Axiomatisations for CCS congruences, Faron Moller
- Self-independent Petri Nets (or a
dead-lock-free paradigm), Sun Yong
- Compositional Characterization of
observable Program Properties, B. Steffen, C.B. Jay, M.
Mendler
- Proving total correctness of
concurrent programs without using auxiliary variables, P.
Paczkowski
- Syntax, typechecking and Dynamic
Semantics for Extended ML, D. Sannella and F. da
Silva
- Formal program development in
Extended ML for the working programmer, D. Sannella
- Timing Concurrent Processes,
C. Tofts
- A Temporal Calculus of
Communicating Systems, Faron Moller and Chris Tofts
- 1990
-
- Probabilistic Non-Determinism,
Claire Jones
- INSTITUTIONS: Abstract Model
Theory for Specification and Programming, R. Burstall and J.
Goguen
- Extending properties to categories
of partial maps, C. Barry Jay
- Relative Frequency in a
Synchronous Calculus, Chris Tofts
- Tactics for State Space Reduction
on the Concurrency Workbench, M.J. Morley
- The Logical Structure of
Sequential Prolog, J. Andrews
- Investigations into proof-search
in a system of first-order dependent function types, D. Pym
and L. Wallen
- Higher-Order Modules and the Phase
Distinction, Harper, Moggi and Mitchell
- An Abstract View of Programming
Languages, E. Moggi
- A Systolic Array for Pyramidal
Algorithms, C. Lengauer and J. Xue
- Local Model Checking for Infinite
State Spaces, Julian Bradfield and Colin Stirling
- On the Description and Development
of One-Dimensional Systolic Arrays, C Lengauer and J.
Xue
- Proving correctness w.r.t.
specifications with hidden parts, Jorge
Farrés-Casals
- An Extended Calculus of
Constructions, Zhaohui Luo
- Relevance Logic and Concurrent
Composition, Mads Dam
- Constructive lambda-Models,
Andreas Knobel
- A Problem of Adequacy:
conservativity of calculus of constructions over higher-order
logic, Zhaohui Luo
- pi-calculus Semantics of
Object-Oriented Programming Languages, David Walker
- Translating CTL* into the modal
mu-calculus, Mads Dam
- The Uniform Proof-Theoretic
Foundation of Linear Logic Programming, James Harland and
David Pym
- Proofs, Search and Computation in
General Logic, David Pym
- Towards a Formal Framework for
Evaluation of Operational Semantics Specifications, Fabio da
Silva
- A Timed Calculus of Communicating
Systems, Liang Chen, Stuart Anderson and Faron
Moller
- The Autosynchronisation of
Leptothorax Acervorum (Fabricius) described in WSCCS, Chris
Tofts
- 1991
-
- Linear Logic and Petri Nets:
Categories, Algebra and Proof, Carolyn Brown
- Semantic Frameworks for
Complexity, Douglas Gurr
- Program Specification and Data
Refinement in Type Theory, Zhaohui Luo
- Computer Assisted Proof for
Mathematics: an Introduction using the LEGO Proof System, R.
Burstall
- Deliverables: an approach to
program development in the Calculus of Constructions, Rod
Burstall and James McKinna
- A Systolizing Compilation
Scheme, C. Lengauer and M. Barnett
- Structuring Specifications
in-the-Large and in-the-Small: Higher-Order Functions, Dependent
Types and Inheritance in SPECTRAL, D. Sannella and B.
Kreig-Bruckner
- Modal Logics for Mobile
Processes, R. Milner, J. Parrow and D. Walker
- The Formalization and Analysis of
a Commmunications Protocol, G. Bruns and S.
Anderson
- Extended ML: Past, present and
future, D. Sannella and A Tarlecki
- A kernel specification formalism
with higher-order parameterisation, D. Sannella and A
Tarlecki
- Proof Methods and Pragmatics for
Parallel Programming, C. Tofts
- Logic Programming: Operational
Semantics and Proof Theory, J Andrews
- Relating Processes with Respect to
Speed, F. Moller and C. Tofts
- Task Allocation in Monomorphic Ant
Species, C. Tofts
- Actions speak louder than words:
Proving Bisimilarity for Context-free Processes, H Huttel
and C Stirling
- Proof Search in the
lambda-Pi-calculus, David Pym and L Wallen
- Correctness-Oriented Approaches to
Software Development, Stephen Gilmore
- The Edinburgh SML Library,
Dave Berry
- Combinators and Bisimulation
Proofs for Restartable Systems, K V S Prasad
- Annotated Transition Systems for
Verifying Concurrent Programs, P. Paczkowski
- Tail recursion via universal
invariants, C Barry Jay
- The Systematic derivation of
Control Signals for Systolic Arrays, C Lengauer and J
Xue
- An Improved Systolic Array for
String Correction, C Lengauer and D Sangiorgi
- A Unifying theory of Dependent
Types I, Z. Luo
- Embedding a CHDDL in a Proof
System, K. Goossens
- The Synthesis of Control Signals
for One-Dimensional Systolic Arrays, J Xue and C
Lengauer
- Modal and Temporal Logics,
Colin Stirling
- Logic Programming in a Fragment of
Intuitionistic Linear Logic; Extended Abstract, D Miller and
J Hodas
- A Logic Programming Language with
Lambda-Abstraction, Function Variables and Simple Unification,
D Miller
- Unification of Simply Typed
Lambda-Terms as Logic Programming, D Miller
- Proof Nets for Multiplicative and
Additive Linear Logic, G Bellin
- A Framework for Defining
Logics, Robert Harper, Furio Honsell and Gordon
Plotkin
- Generating Program Animators from
Programming Language Semantics, D. Berry
- An Analysis of a Monte Carlo
Algorithm for Estimating the Permanent, M. Jerrum
- Mechanizing Proof Theory:
Resource-Aware Logics and Proof-Transformations to extract implicit
information, G. Bellin
- Classes of Systolic Y-Tree
Automata and a Comparison with Systolic trellis Automata,
Sangiorgi, Fachini and Schettina
- A Decision Procedure Revisited:
Notes on Direct Logic, Linear Logic and its Implementations,
G Bellin and J Ketonen
- The Uniform Proof-theoretic
Foundation of Linear Logic Programming (Extended Abstract),
J Harland and D Pym
- Undecidable Equivalences for Basic
Process Algebra, J F Groote and H Huttel
- On Hereditary Harrop Formulae as a
Basis for Logic Programming, J Harland
- Domain Theory in Realizability
Toposes, Wesley Phoa
- Verifying Temporal Properties of
Systems with Applications to Petri Nets, Julian C
Bradfield
- Silence is Golden: Branching
Bisimilarity is Decidable for Context-free Processes, Hans
Huttel
- A Distributed Concurrent
Implementation of Standard ML, D. Matthews
- A Language for value-passing
CCS, Glenn Bruns
- Recent Developments in Systolic
Design, C. Lengauer and J. Xue
- Modularizing the Specification of
a Small Database System in Extended ML, E.
Kazmierczak
- Improved bounds for mixing rates
of Markov chains and multicommodity flow, Alistair
Sinclair
- A Mildly Exponential Approximation
Algorithm for the Permanent, M. Jerrum
- The Polyadic pi-Calculus: A
Tutorial, Robin Milner
- Coherence in Category Theory and
the Church-Rosser Property, C B Jay
- Fixpoint and Loop Constructions as
Colimits, C B Jay
- Long Bn Normal Forms and
Confluence, C B Jay
- An Interleaving Model for
Real-Time Systems, Chen Liang
- Decidability and Completeness in
Real-Time Processes, Chen Liang
- Modelling British Rail's
Interlocking Logic: Geographic Data Correctness, M
Morley
- Modelling Reduction in Confluent
Categories, C B Jay
- An Ideal Model for an Extended
Lambda-Calculus with Refinement, J Agusti et al
- The Lazy Lambda Calculus in a
Concurrency Scenario, D Sangiorgi
- An n-Categorical Pasting
Theorem, J Power
- Decidability, Behavioural
Equivalences and Infinite Transition Graphs, Hans
Hüttel
- 1992
-
- Semantics of Local Variables,
R D Tennent and O'Hearn
- Verification of Parallel Systems
via Decomposition, J F Groote and F Moller
- First Order Linear Logic in
Symmetric Monoidal Closed Categories, Simon Ambler
- Formal Program Development in
Modular Prolog: A Case Study, M Read and E
Kazmierczak
- Ordinal Complexity of Recursive
Programs and their Termination Proofs, M Fairtlough
- Loop Parallelization and
Unimodularity, C. Lengauer and M. Barnett
- Efficient Algorithms for Listing
Combinatorial Structures, Leslie Ann Goldberg
- A Proof Assistant for Symbolic
Model-Checking, J C Bradfield
- Intersection Types and Bounded
Polymorphism, Benjamin Pierce
- Approximating the Permanent: a
Simple Approach, L E Rasmussen
- A Unifying Theory of Dependent
Types: the Schematic Approach, Zhaohui Luo
- The Formal Synthesis of Control
Signals for Systolic Arrays, Jingling Xue
- Toward Formal Development of
Programs from Algebraic Specifications: Model-Theoretic
Foundations, D. Sannella and A Tarlecki
- Tail Recursion through Universal
Invariants, C B Jay
- A Set-theoretic Setting for
Structuring Theories in Proof Development, Z. Luo and R.
Burstall
- A Framework for Binding
Operators, Sun Yong
- An introduction to fibrations,
topos theory, the effective topos and modest sets, Wesley
Phoa
- Inductive Data Types:
Well-ordering Types Revisited, H. Goguen and Zhaohui
Luo
- Listing Graphs that Satisfy First
Order Sentences, L A Goldberg
- LEGO Proof Development System:
User's Manual, Zhaohui Luo and R Pollack
- On Resolution in Fragments of
Classical Linear Logic (Extended Abstract), J Harland and D
J Pym
- A proposed categorical semantics
for Pure ML, Wesley Phoa and Michael Fourman
- From term models to domains,
Wesley Phoa
- Building domains from graph
models, Wesley Phoa
- Process-Algebraic Interpretations
of Positive Linear and Relevant Logics, Mads Dam
- CTL* and ECTL* as fragments of the
modal mu-calculus, Mads Dam
- Bisimulation Equivalence is
Decidable for all Context-Free Processes, Soren Christensen,
Hans Hüttel, Colin Stirling
- Unlimp - Uniqueness as a Leitmotiv
for Implementation, Stefan Kahrs
- Verification in ASL and related
specification languages, Jorge Farrés-Casals
- Modal and Temporal Logics for
Processes, Colin Stirling
- Toward formal development of
programs from algebraic specifications: parameterisation
revisited, Donald Sannella, Stefan Sokolowski and Andrzej
Tarlecki
- Relational Parametricity and Local
Variables, P W O'Hearn and R D Tennent
- Fixpoints of Büchi
automata, Mads Dam
- Object-Oriented Programming
Without Recursive Types, Benjamin C Pierce and David N
Turner
- An Abstract View of Objects and
Subtyping , Martin Hofmann and Benjamin C Pierce
- Representing Logics in Type
Theory, Philippa Gardner
- Formal Development of Functional
Programs in Type Theory - A Case Study, Martin
Hofmann
- A Unification Algorithm for the
lambda-Pi-Calculus, David Pym
- Brewing Strong Normalization
Proofs with LEGO, Thorsten Altenkirch
- Opeerational Semantics Based
Formal Symbolic Simulation, K G W Goossens
- On the pi-Calculus and Linear
Logic, G Bellin and P J Scott
- Correctness Proofs of Compilers
and Debuggers: an Overview of an Approach Based on Structural
Operational Semantics, Fabio Q B da Silva
- A Sub-logarithmic Communication
Algorithm for the Completely Connected Optical Communication
Parallel Computer, Leslie Ann Goldberg and Mark
Jerrum
- Functional Compilation from the
Standard ML Core Language to Lambda Calculus, Nick
Rothwell
- Parsing in the SML Kit,
Nick Rothwell
- Miscellaneous Design Issues in the
ML Kit, Nick Rothwell
- Polymorphic Type Checking by
Interpretation of Code, Stefan Kahrs
- A Case Study in Safety-Critical
Design, Glenn Bruns
- Observational Equivaalence and
Compiler Correctness, Fabio Q B da Silva
- Correctness Proofs of Compilers
and Debuggers: an Approach Based on Structural Operational
Semantics, Fabio Q B da Silva
- Deliverables: a categorical
approach to program development in type theory, Rod Burstall
and James McKinna
- The Virtues of Eta-expansion,
C Barry Jay and Neil Ghani
- Decomposability, Decidability and
Axiomatisability for Bisimulation Equivalence on Basic Parallel
Processes, S Christensen, Y Hirshfield and F Moller
- A Semantics for Static Type
Inference, Gordon Plotkin
- Logic Programming via Proof-Valued
Computations, David J Pym and Lincoln A Wallen
- Deliverables: a categorical
approach to program development in type theory, James Hugh
McKinna
- A Synopsis on the Identification
of Linear Logic Programming Languages, James Harland and
David Pym
- Action Structures, Robin
Milner
- An Algorithm for Constructing
beta-eta-long normal forms, Philippa Gardner
- Equivalences between Logics and
their Representing Type Theories, Philippa Gardner
- Newtonian Arbiters Cannot be
Proven Correct, Michael Mendler and Terry Stroup
- Hiding and Behaviour: An
Institutional Approach, Rod Burstall and Razvan
Diaconescu
- 1993
-
- Enrichment Through Variation,
R. Gordon and A. J. Power
- A Modal Logic for Handling
Behavioural Constraints in Formal Hardware Verification,
Michael Mendler
- Statically Types Friendly
Functions via Partially Abstract Types, B C Pierce and D N
Turner
- Mistakes and Ambiguities in the
Definition of Standard ML, Stefan Kahrs
- PAC-Learning Geometrical
Figures, Paul W Goldberg
- Approximately Counting Hamilton
Cycles in Dense Graphs, Martin Dyer, Alan Frieze and Mark
Jerrum
- Simulated Annealing for Graph
Bisection, Mark Jerrum and Gregory Sorkin
- Decidability Questions for
Bisimilarity of Petri Nets and Some Related Problems, Petr
Jancar
- Algebraic Theories for
Name-Passing Calculi, Joachim Parrow and Davide
Sangiorgi
- Literate Programming: A
Review, Angus Duggan
- Action Structures for the
pi-Calculus, Robin Milner
- Errata and Remarks, David J
Pym
- Expressing Mobility in Process
Algebras: First-Order and Higher-Order Paradigms, Davide
Sangiorgi
- Correctness of Data
Representations in Algol-like Languages, R D
Tennent
- Embedding Hardware Description
Languages in Proof Systems, Kees G W Goossens
- The Formalisation of a Hardware
Description Language in a Proof System: Motivation and
Applications, Kees G W Goossens
- A Theory of Bisimulation for the
pi-calculus, Davide Sangiorgi
- Timed Processes: Models, Axioms
and Decidability, Liang Chen
- Uniform sampling modulo a group of
symmetries using Markov chain simulation, Mark
Jerrum
- Structure and Behaviour in
Hardware Verification, K G W Goossens
- On the decidability of model
checking for several mu-calculi and Petri Nets, Javier
Esparza
- Multiple Inheritance via
Intersection Types, Adriana B Compagnoni and Benjamin C
Pierce
- Undecidable Equivalences for Basic
Parallel Processes, Hans Hüttel
- Fibrations, Logical Predicates and
Indeterminates, Claudio Alberto Hermida
- Decidability and Decomposition in
Process Algebras, Soren Christensen
- Constructions, Inductive Types and
Strong Normalization, Thorsten Altenkirch
- 1994
-
- Higher-Order Subtyping,
Martin Steffen and Benjamin Pierce
- Subtyping in F-omega-Meet is
decidable, Adriana B Compagnoni
- Locality and Non-interleaving
Semantics in calculi for mobile processes, Davide
Sangiorgi
- Interfaces and Extended ML,
Stefan Kahrs, Donald Sannella and Andrzej Tarlecki
- First-Class Polymorphism for
ML, Stefan Kahrs
- The Mobility Workbench. A tool for
the pi-Calculus, Björn Victor and Faron Moller
- A polynomial algorithm for
deciding bisimilarity of normed context-free processes,
Yoram Hirshfeld, Mark Jerrum and Faron Moller
- Applying Process Refinement to a
Safety-Relevant System, Glenn Bruns
- A polynomial-time algorithm for
deciding bisimulation equivalence of normed Basic Parallel
Processes, Yoram Hirshfeld, Mark Jerrum and Faron
Moller
- Why tricategories?, A J
Power
- A very simple algorithm for
estimating the number of k-colourings of a low-degree graph,
Mark Jerrum
- Congruences in Commutative
Semigroups, Yoram Hirshfeld
- Improved approximation algorithms
for MAX k-CUT and MAX BISECTION, Alan Frieze and Mark
Jerrum
- On modal mu-calculus and
Büchi tree automata, Roope Kaivola
- Deciding equivalences in simple
Process Algebras, Yoram Hirshfeld
- Trapping Mutual Exclusion in the
Box Calculus, Javier Esparza and Glenn Bruns
- The Computational Complexity of
Counting, Mark Jerrum
- A fully abstract semantics for
causality in the pi-calculus, Michele Boreale and Davide
Sangiorgi
- High Undecidability of Weak
Bisimilarity for Petri Nets, Petr Jancar
- On the Bisimulation Proof
Method, Davide Sangiorgi
- The Definition of Extended ML,
Stefan Kahrs, Donald Sannella, Andrzej Tarlecki
- An Old Sub-Quadratic Algorithm for
Finding Extremal Sets, Paul Pritchard
- Decidability of Model Checking for
Infinite-State Concurrent Systems, Javier Esparza
- Positive Subtyping, Martin
Hofmann and Benjamin Pierce
- A Typed Operational Semantics for
Type Theory, Healfdene Goguen
- Balancing Load under Large and
Fast Load Changes in Distributed Computing Systems, Thierry
Le Sergent and Bernard Berthomieu
- Adaptive selection of protocols
for strict coherency in distributed shared memory, Thierry
Le Sergent and David C J Matthews
- Axiomatic Domain Theory in
Categories of Partial Maps, Marcelo P. Fiore
- The Proof Theory and Semantics of
Intuitionistic Modal Logic, Alex K. Simpson
- On Computing the Subset Graph of a
Collection of Sets, Paul Pritchard
- Supporting Formal Reasoning about
Standard ML, Graham Collins and Stephen Gilmore
- Concurrency in a Natural
Semantics, Kevin Mitchell
- Multiple Values in Standard
ML, Kevin Mitchell
- Generating and counting Hamilton
cycles in random regular graphs, Alan Frieze, Mark Jerrum,
Michael Molloy, Robert Robinson and Nicholas Wormald
- 1995
-
- Towards a Domain Theory for
Termination Proofs, Stefan Kahrs
- Correct Separate and Selective
Closure Conversion, Paul Steckler
- LEMMA Interface Definition,
David C J Matthews and Thierry Le Sergent
- Computational Pólya
Theory, Mark Jerrum
- On behavioural abstraction and
behavioural satisfaction in higher-order logic, Martin
Hofmann and Donald Sannella
- Proof and Design, Michael
P. Fourman
- Typing Abstract Data Types,
Judith Underwood
- Tableau for Intuitionistic
Predicate Logic as Metatheory, Judith Underwood
- The definition of Extended ML: a
gentle introduction, Stefan Kahrs, Donald Sannella and
Andrzej Tarlecki
- The Theory of LEGO, Robert
Pollack
- Axiomatising Linear Time
Mu-calculus, Roope Kaivola
- LEMMA: A Distributed Shared Memory
with Global and Local Garbage Collection, David C J Matthews
and Thierry Le Sergent
- A quasi-polynomial-time algorithm
for sampling words from a context-free language, Vivek Gore
and Mark Jerrum
- Extensional concepts in
intensional type theory, Martin Hofmann
- The Algebra of Finite State
Processes, Peter Michael Sewell
- Formal Derivation of a Class of
Computers, Li-Guo Wang
- Lax naturality through
enrichment, Yoshiki Kinoshita and John Power
- First Steps on the Representation
of Domains, Marcelo P Fiore
- Realizability Toposes and Language
Semantics, John R. Longley
- Formal Design of a Class of
Computers, Li-Guo Wang and Michael Mendler
- Abstraction of Hardware
Construction, Li-Guo Wang and Michael Mendler
- Papers on Poly/ML, David C
J Matthews
- Universal Structure and a
Categorical Framework for Type Theory, Makoto
Takeyama
- An effective tableau system for
the linear time mu-calculus, Julian Bradfield, Javier
Esparza and Angelika Mader
- On the expressivity of the modal
mu-calculus, Julian Bradfield
- Adjoint rewriting, Neil
Ghani
- 1996
-
- Detecting Local Channels in
Distributed Poly/ML, Paul Steckler
- Partial Functions in a Total
Setting, Simon Finn, Michael Fourman and John
Longley
- Algebraic Structure for Bicategory
Enriched Categories, R Gordon and A J Power
- A New Approach to Polynomial-time
Generation of Random Points in Convex Bodies, Russ Bubley,
Martin Dyer and Mark Jerrum
- Standard ML Type Generativity as
Existential Quantification, Claudio Russo
- The Polymorphic Pi-Calculus:
Theory and Implementation, David Turner
- Computational applications of
calculi based on monads, Pietro Cenciarelli
- Dual Intuitionistic Linear
Logic, Andrew Barber
- Safety Assurance in Interlocking
Design, Matthew John Morley
- The Swendsen-Wang process does not
always mix rapidly, Vivek Gore and Mark Jerrum
- Graph Types for Monadic Mobile
Processes, Nobuko Yoshida
- The Theory of Interacting
Deductions and its Application to Operational Semantics,
Andrew Wilson
- 1997
-
- Decidability of Bisimulation
Equivalence for Normed Pushdown Processes, Colin
Stirling
- Logical Full Abstraction and
PCF, John Longley and Gordon Plotkin
- A Type-Theoretic Analysis of
Modular Specifications, Savitri Maharaj
- Model Checking the Full Modal
Mu-Calculus for Infinite Sequential Processes, Olaf Burkart
and Bernhard Steffen
- Using Automata to Characterise
Fixed Point Temporal Logics, Roope Kaivola
- Sequent Combinators: A Hilbert
System for the Lambda Calculus, Healfdene Goguen
- Candidates for Substitution,
Healfdene Goguen and James McKinna
- Some Lambda Calculus and Type
Theory Formalized, James McKinna and Robert Pollack
- Models of Sharing Graphs: A
Categorical Semantics of let and letrec, Masahito
Hasegawa
- Typed Operational Semantics for
Higher Order Subtyping, Adriana Compagnoni and Healfdene
Goguen
- The C-LEMMA Memory Interface on
the Cray T3D, Christopher D. Walton and Bruce J.
McAdam
- Subject Reduction and Minimal
Types for Higher Order Subtyping, Adriana
Compagnoni
- Programming in Standard ML '97: A
Tutorial Introduction, Stephen Gilmore
- Decidable Higher Order
Subtyping, Adriana Compagnoni
- Relative Equational Specification
and Semantics, Jo Erskine Hannay
- The modal mu-calculus alternation
hierarchy is strict, J.C. Bradfield
- Implementing Proof by Pointing
without a Structure Editor, Yves Bertot, Thomas
Kleymann-Schreiber and Dilip Sequeira
- The Verification of Asynchronous
Circuits using CCS, Graham Clark and George Taylor
- Subtyping Dependent Types,
David Aspinall and Adriana Compagnoni
- Linear Type Theories, Semantics
and Action Calculi, Andrew Barber
- Lecture Notes on Formal Program
Development, Stefan Kahrs
- Using Markovian Process Algebra to
Specify Interactions in Queueing Systems, Nigel Thomas and
Jane Hillston
- PCF extended with real numbers: a
domain-theoretic approach to higher-order exact real number
computation, Martín Hötzel
Escardó
- That About Wraps it Up: Using FIX
to Handle Errors Without Exceptions, and Other Programming
Tricks, Bruce J. McAdam
- Categorical Structure of
Continuation Passing Style, Hayo Thielecke
- Elementary structural analysis for
PEPA, Stephen Gilmore, Jane Hillston and Laura
Recalde
- Dynamic ML without Dynamic
Types, Stephen Gilmore, Dilsun Kirli and Christopher
Walton
- Machine Assisted Proofs for
Generic Semantics to Compiler Transformation Correctness
Theorems, Saif Ullah Kahn
- 1998
-
- Process Abstraction in the
Verification of Temporal Properties, Glenn R. Bruns
- Notes on Simply Typed Lambda
Calculus, Ralph Loader
- A Class of PEPA Models Exhibiting
Product Form Solution over Submodels, Jane Hillston
- Injective spaces and the filter
monad, Martín Hötzel Escardó
- On the Unification of
Substitutions in Type-Inference, Bruce J. McAdam
- Simplifying the modal mu-calculus
alternation hierarchy, Julian C. Bradfield
- Bisimulation equivalence is
decidable for normed Process Algebra, Yoram Hirshfeld and
Mark Jerrum
- The ``Burnside process'' converges
slowly, Leslie Ann Goldberg and Mark Jerrum
- A Manufacturing Production Line
with Service Interruptions, Nigel Thomas and Isi
Mitrani
- Types For Modules, Claudio
V. Russo
- Applicative Notions in ML-like
Programs, Budi Halim Ling
- On counting independent sets in
sparse graphs, Martin Dyer, Alan Frieze and Mark
Jerrum
- Hoare Logic and VDM:
Machine-Checked Soundness and Completeness Proofs, Thomas
Kleymann
- Metatheory of Verification Calculi
in LEGO: To What Extent Does Syntax Matter?, Thomas
Kleymann
- Learning Function Free Horn
Expressions, Roni Khardon
- Learning Range Restricted Horn
Expressions, Roni Khardon
- Categorical Term Rewriting: Monads
and Modularity, Christoph Lüth
- Equivalence semantics for
concurrency: comparison and application, Vashti Christina
Galpin
- Referential Opacity in Equational
Reasoning, Jo Erskine Hannay
- Hoare Logic and Auxiliary
Variables, Thomas Kleymann
- Direct models for the
computational lambda-calculus, Carsten
Führmann
- Nested Sketches, Horst
Reichel
- The sequentially realizable
functionals, John Longley
- Type Inference with Bounded
Quantification, Dilip Sequeira
- 1999
-
- Diluting ACID, Tim
Kempster, Colin Stirling and Peter Thanisch
- Pre-logical Relations,
Furio Honsell and Donald Sannella
- Type Systems For Polynomial-time
Computation, Martin Hofmann
- Architectural Specifications in
CASL, Michel Bidoit, Donald Sannella and Andrzej
Tarlecki
- Decidability and complexity of
equivalences for simple process algebras, Jitka
Stríbrná
- A Semantic analysis of
control, James David Laird
- Abstract Machines for Memory
Management, Christopher Walton
- Decidability of DPDA
equivalence, Colin Stirling
- A Theory of Program
Refinement, Ewen Denney
- A Polymorphic Type and Effect
System for Detecting Mobile Functions, Dilsun Kirli
- Fully Complete Models for ML
Polymorphic Types, Samson Abramsky and Marina
Lenisa
- Graphs for Recording Type
Information, Bruce J. McAdam
- Proving Correctness of Modular
Functional Programs, Christopher Owens
- Counting unlabelled subtrees of a
tree is #P-complete, Leslie Ann Goldberg and Mark
Jerrum
- 2000
-
- 2001
-
- 2002
-
- 2003
-
- 2004
-
An error occured whilst processing this directive