Edinburgh BRA Publications
1995

David Aspinall
and
Adriana Compagnoni,
Subtyping Dependent Types.
To appear in LICS 1996.

Andrew Barber,
Dual Intuitionistic Linear Logic.
To be submitted to the Journal of Logic and Functional Programming, 1995.

Philippa Gardner,
Equivalences between Logics and their Representing Type Theories.
To appear in Mathematical Structures in Computer Science, 1995.

R. Gordon
and
John Power,
Enrichment through variation.
To appear in J. Pure Appl. Algebra.

Elsa Gunter
and
Savitri Maharaj,
Studying the ML module system in HOL.
The Computer Journal, 38(2), 1995.

Masahito Hasegawa,
Decomposing typed lambdacalculus into a couple of categorical programming languages.
In Peter Dybjer and Randy Pollack, editors,
Informal Proceedings of the Joint CLICSTYPES workshop
on categories and type theory,
Programming Methodology Group Reports 85.
Göteborg University and Chalmers University of Technology, 1995.

Zhaohui Luo,
Algorithms refinement in type theory.
Manuscript in preparation.

Savitri Maharaj,
A TypeTheoretic Analysis of Modular Specifications.
Forthcoming PhD thesis, The University of Edinburgh, 1995.

Conor McBride,
Inverting inductively defined predicates in LEGO.
Master's thesis, University of Edinburgh, 1995.

James McKinna,
Checking algorithms for Pure Type Systems revisited.
Manuscript in preparation, 1995.

James McKinna,
Typed lambdacalculus formalised: ChurchRosser and Standardisation theorems.
Manuscript in preparation, 1995.

Dale Miller,
Gordon Plotkin
and
David Pym,
A Linear Analysis of Natural Deduction (to appear).

John Power,
Gordon, R.,
and
Street, R. H.,
Coherence for Tricategories.
Memoirs Amer. Math. Soc. (to appear).

John Power,
Why Tricategories?
Information and Computation Vol. 120, No.2, pp. 251262.

Makoto Takeyama.
Universal Structure and a Categorical Framework for Type Theory.
PhD thesis, University of Edinburgh, 1995.

Healfdene Goguen,
Typed Operational Semantics.
Proceedings of TLCA 1995, LNCS 902.

Martin Hofmann,
Extensional concepts in intensional type theory,
Abstract,
Ph.D. Thesis, University of Edinburgh.

Randy Pollack,
A Verified Typechecker,
Proceedings of TLCA 1995, LNCS 902.
1994

L.S. van Benthem Jutting,
James McKinna and
Randy Pollack,
Checking Algorithms for Pure Type Systems,
Types for Proofs and Programs:
International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers.
Henk Barendregt and
Tobias Nipkow (editors),
pages 1961, LNCS 806, SpringerVerlag.

Rod Burstall,
Terms, Proofs and Refinement (Invited paper).
LICS 1994.

Rod Burstall
and
Razvan Diaconescu,
Hiding and Behaviour: an Institutional Approach.
A classical mind: essays in honour of C.A.R. Hoare,
A.W. Roscoe (ed.), PrenticeHall, 1994.

Adriana Compagnoni.
Subtyping in Fomegawedge is decidable.
Technical Report ECSLFCS94281, LFCS, University of Edinburgh, January 1994.
To appear in the proceedings of Computer Science Logic, 1994.

Pietro Cenciarelli,
A modular development of denotational semantics in LEGO.
Presented at the Types for Proofs and Programs Workshop, Båstad,
June 1994.

Philippa Gardner,
Discovering Needed Reductions Using Type Theory.
Theoretical Aspects of Computer Science,
LNCS 789, SpringerVerlag, 1994.

Healfdene Goguen,
A Typed Operational Semantics for Type Theory,
Abstract, Ph.D. Thesis, LFCS Technical Report ECSLFCS94304.

Martin Hofmann,
Elimination of extensionality in MartinL{\"o}f type theory.
Types for Proofs and Programs:
International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers.
Henk Barendregt and
Tobias Nipkow (editors),
LNCS 806, SpringerVerlag.

Martin Hofmann
and
Thomas Streicher,
A Groupoid Model Refutes Uniqueness of Identity Proofs.
LICS 1994.

Zhaohui Luo,
Computation and Reasoning: A Type Theory for Computer Science.
International Series of Monographs on Computer Science, 11.
Oxford University Press, 1994. (ISBN 0 19 853835 9).

Savitri Maharaj,
Encoding Zstyle schemas in UTT.
In Types for Proofs and Programs, LNCS 806.
SpringerVerlag, 1994.

Gordon Plotkin,
A Semantics for Static Type Inference.
Information and Computation,
Vol.109,
Nos.12,
pp. 256299,
1994.

Pietro di Gianantonio,
Furio Honsell,
Silvia Liani
and
Gordon Plotkin,
Countable NonDeterminism and Uncountable Limits.
In Proceedings of the conference ``CONCUR '94'' on concurrency theory,
pp. 130145.
LNCS 836, SpringerVerlag, Berlin/New York, 1994.

Randy Pollack,
The Theory of LEGO,
Ph.D. Thesis, University of Edinburgh, 1994.

Randy Pollack,
Incremental Changes in LEGO: 1994.
More recent changes are documented here.

Robert Pollack,
Closure Under AlphaConversion,
Types for Proofs and Programs:
International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers.
Henk Barendregt and
Tobias Nipkow (editors),
pp. 313332, LNCS 806, SpringerVerlag.

Christophe Raffalli.
L'arithmétique fonctionnelle du second ordre avec points fixes.
Ph.D. thesis, Université Paris 7, Février 1994.

Alex Simpson,
The Proof Theory and Semantics of Intuitionistic Modal Logic.
Ph.D. thesis,
LFCS technical report number ECSLFCS94308,
University of Edinburgh, 1994.
1993

Thorsten Altenkirch,
A formalization of the strong normalization proof for
system F in LEGO.
Proceedings of TLCA 1993.

Thorsten Altenkirch,
Constructions, Inductive Types and Strong Normalization.
Ph.D. thesis, University of Edinburgh,
ECSLFCS93279, 1993.

Rod Burstall
and
James McKinna,
Deliverables: a Categorical Approach to Program Development in Type Theory,
Proceedings of the international symposium on Mathematical Foundations of Computer Science,
MFCS 1993, Gdansk, Poland, Sept. 1993.
A. Borzyszkowski and S. Sokolowski (eds),
pp. 3267, LNCS 711, SpringerVerlag.

Adriana B. Compagnoni
and
Benjamin C. Pierce.
Multiple inheritance via intersection types.
Technical Report ECSLFCS93275, LFCS, University of Edinburgh, August 1993.
Also available as Catholic University Nijmegen computer science technical report 9318.

Philippa Gardner,
A New Type Theory for Representing Logics.
Fourth International Conference on Logic Programming and Automated Reasoning,
LNAI 698, SpringerVerlag, 1993.

Healfdene Goguen
and
Zhaohui Luo,
Inductive Data types: WellOrdering Types Revisited.
In
G. Huet
and
Gordon Plotkin
(eds.),
Logical Environments,
Cambridge University Press,
1993.
Also as
ECSLFCS92209,
Dept. of Computer Science,
University of Edinburgh.

R. Harper,
F. Honsell
and
Gordon Plotkin,
A Framework for Defining Logics.
Journal of the Association of Computing Machinery, Vol.40, No.1,
pp. 143184, 1993.

G. Huet
and
Gordon Plotkin
(eds).
Logical Environments.
Cambridge University Press, 1993.

Claudio Hermida.
Fibrations, Logical Predicates and Indeterminates.
Ph.D. thesis, ECSLFCS93277,
University of Edinburgh, 1993.

Zhaohui Luo,
Program specification and data refinement in type theory.
Mathematical Structures in Computer Science, 3(3), 1993.
An earlier version appears in Proc. of TAPSOFT'91, LNCS 493,
and also as
ECSLFCS91131,
Dept of Computer Science,
University of Edinburgh.

Gordon Plotkin,
Type Theory and Recursion (Abstract).
In Proceedings of the Eighth Symposium on Logic in Computer Science,
Montreal, p. 374.
Washington, IEEE Computer Society Press, 1993.

James McKinna
and
Randy Pollack,
Pure Type Systems Formalized,
Proceedings of TLCA 1993

Randy Pollack
and
Claire Jones,
Incremental Changes in LEGO.
Further changes are documented
here.

G.M. Kelly
and
John Power,
Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads.
J. Pure Appl. Algebra,
Vol 89,
pp. 163179,
1993.

Christophe Raffalli.
Machine deduction.
International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers.
Henk Barendregt and
Tobias Nipkow (eds.),
LNCS 806, SpringerVerlag.

Christophe Raffalli.
Data types, infinity and equality in system AF2.
To appear in the Proceedings of CSL'93, Swansea, UK, September 1993.
1992

Thorsten Altenkirch,
Brewing Strong Normalization Proofs with LEGO,
Abstract,
LFCS Technical Report
ECSLFCS92230.

Martin Hofmann,
Formal Development of Functional Programs in Type Theory 
A Case study,
Abstract,
LFCS Technical Report
ECSLFCS92228.

Rod Burstall
and
James McKinna,
Deliverables: A categorical approach to program development in type theory,
Introduction,
LFCS Technical Report
ECSLFCS9224.

Zhaohui Luo,
A Unifying Theory of Dependent Types: the schematic approach.
Proc. of Symp. on Logical Foundations of Computer Science
(Logic at Tver'92), LNCS 620, 1992.
Also as
ECSLFCS92202,
Dept of Computer Science,
University of Edinburgh.
LFCS Technical Report
ECSLFCS92202.

Zhaohui Luo
and
Randy Pollack,
LEGO Proof Development System: User's Manual,
LFCS Technical Report
ECSLFCS92211.
Notice that changes are documented
here.

James McKinna,
Deliverables: a categorical approach to program development in type theory
,
Abstract, Ph.D. Thesis, University of Edinburgh.

Randy Pollack,
Typechecking in Pure Type Systems,
Proceedings of the 1992 Workshop on Types for Proofs and Programs,
Båstad

Randy Pollack,
Implicit Syntax.
An earlier version of this paper appeared in the
Proceedings of the First Workshop on Logical Frameworks, Antibes,
May 1990, Gérard Huet and
Gordon Plotkin (editors).
1991

Rod Burstall,
Computer Assisted Proof for Mathematics:
an Introduction using the LEGO Proof System,
Abstract,
LFCS Technical Report
ECSLFCS91142.

Robert Harper and
Randy Pollack,
Type Checking with Universes
, TCS, Volume 89, pages 107136.

Zhaohui Luo,
Program Specification and Data Refinement in Type Theory,
TapSoft 1991.
 Michael Mendler,
Constrained proofs: a logic for dealing with behavioural constraints in formal hardware verification,
Workshop on Designing Correct Circuits, SpringerVerlag.
1990

Zhaohui Luo,
Higherorder Calculus and Theory Abstraction.
Information and Computation 90(1), 1990.

Zhaohui Luo,
An Extended Calculus of Constructions.
Ph.D. thesis,
ECSLFCS90118,
University of Edinburgh, 1990.
Also as Report CST6590,
Dept of Computer Science,
University of Edinburgh.

Savitri Maharaj,
Implementing Z in LEGO.
Master's thesis, University of Edinburgh, 1990.

Zhaohui Luo,
A Problem of Adequacy: conservativity of calculus of constructions over higherorder logic.
ECSLFCS90121,
Dept of Computer Science,
University of Edinburgh.
1989
Last updated on 5 March 1996 by
Healfdene Goguen
<hhg@dcs.ed.ac.uk>