Next: Example proof developments
Up: Contents
Previous: LEGO System and documentation
LEGO Literature
Please notify us of any
new/missing reference, including your own contributions!
2000
1999
1998
1997
 Yves
Bertot,
Thomas KleymannSchreiber and Dilip Sequeira.
Implementing Proof by Pointing without a Structure
Editor. LFCS Technical Report
ECSLFCS97368. Also published as Rapport de recherche de l'INRIA
Sophia
Antipolis RR3286.
 Savitri Maharaj,
A Typetheoretic Analysis of Modular Specifications.
PhD thesis, the University of Edinburgh, 1996. ECSLFCS97354.
Abstract.

Wolfgang Naraschewski. Towards an Objectoriented Progification Language. In The 1997 International Conference on
Theorem Proving in Higher Order Logics, USA.

Thomas Schreiber.
Auxiliary Variables and Recursive Procedures. In
TAPSOFT'97:
Theory and Practice of Software Development, volume
1214 of Lecture Notes in Computer Science, pages 697711, Lille, France, April 1997. Springer.
 Shenwei Yu and Zhaohui Luo.
Implementing
a model checker for Lego. Proc. of Formal Methods Europe 97
(FME'97), Austria, 1997.
1996

Martin Hofmann,
Wolfgang Naraschewski,
Martin Steffen
and Terry Stroup.
Inheritance of proofs. Technical Report IMMDVII5/96,
Informatik VII,
Universität ErlangenNürnberg.
Presented at the Third
International Workshop on Foundations of ObjectOriented Languages.
Submitted to a special issue of Theory and Practice of Objectoriented
systems (TAPOS).
 Zhaohui Luo.
Coercive subtyping in type theory.
Proc. of CSL'96,
the 1996 Annual Conference of the European Association for
Computer Science Logic, Utrecht.

Nikos Mylonakis.
Adequate encodings of proof systems for algebraic specifications in UTT.
CADE13 Workshop on Proof Search in TypeTheoretic Languages.
 Randy Pollack,
Theories in Type Theory,
Transparencies for a talk.

Bernhard Reus,
Synthetic Domain Theory in Type Theory:
Another Logic of Computable Functions,
In Theorem Proving in Higher Order Logics:
9th International Conference, TPHOLs'96, volume 1125 of
Lecture Notes in Computer Science,
pages 363381. SpringerVerlag.
1995

Pietro Cenciarelli ,
Computational applications of calculi based on monads, Thesis.

Healfdene Goguen,
The Metatheory of UTT,
In Types for Proofs and Program,
volume 996 of Lecture Notes in Computer Science,
pages 6082. SpringerVerlag.
 Martin Hofmann, Extensional concepts in intensional type theory, Abstract, Thesis
 Randy Pollack,
A Verified Typechecker
, TLCA'95.

Bernhard Reus,
Program Verification in Synthetic Domain
Theory, Thesis.
 Makoto Takeyama,
Universal Structure and a Categorical Framework for Type Theory,
Thesis.
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
 Healfdene Goguen,
A Typed Operational Semantics for Type Theory,
Abstract, PhD Thesis, LFCS Technical Report ESCLFCS94304
 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)

Randy Pollack,
The Theory of LEGO
, Thesis
 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),
pages 313332, LNCS 806, SpringerVerlag
1993

Thorsten
Altenkirch,
A formalization of the strong normalization proof for system
F in LEGO, TLCA'93.
 Thorsten Altenkirch, Constructions, Inductive Types and Strong Normalization, Thesis
 H. 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,
Edinburgh University.
 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,
Edinburgh University.
[Click here
for its dvifile.]
 James McKinna and Randy Pollack,
Pure Type Systems Formalized
, TLCA'93
 Randy Pollack and
Claire Jones,
Incremental Changes in LEGO.
Further changes are documented here.

Bernhard Reus and Thomas Streicher,
Verifying Properties of Module Construction in Type Theory,
Abstract,
in MFCS'93, Springer, LNCS volume 711.
1992
 Thorsten Altenkirch, Brewing Strong Normalization Proofs with LEGO, Abstract, LFCS Technical Report ECSLFCS92230. This is in many ways superseded by
the paper presented at TLCA'93 but contains some comments on the proof for simply typed lambda calculus.
 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,
Edinburgh University.
Univ.
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, Thesis
 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 ECSLFCS91132
 Robert Harper and
Randy Pollack,
Type Checking with Universes
, TCS, Volume 89, pages 107136
 Claire Jones,
Completing the rationals and metric spaces in LEGO, in
Gérard Huet, Gordon Plotkin and Claire Jones, eds,
Proceedings of the Second Workshop on Logical Frameworks, pp. 209222.
 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, Springer.
1990
1989
1988
Last modified: Mon Sep 7 15:21:34 BST 1998
by the LEGO Team
<lego@dcs.ed.ac.uk>