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 Kleymann-Schreiber and Dilip Sequeira.
Implementing Proof by Pointing without a Structure
Editor. LFCS Technical Report
ECS-LFCS-97-368. Also published as Rapport de recherche de l'INRIA
Sophia
Antipolis RR-3286.
- Savitri Maharaj,
A Type-theoretic Analysis of Modular Specifications.
PhD thesis, the University of Edinburgh, 1996. ECS-LFCS-97-354.
Abstract.
-
Wolfgang Naraschewski. Towards an Object-oriented 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 697-711, 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 IMMDVII-5/96,
Informatik VII,
Universität Erlangen-Nürnberg.
Presented at the Third
International Workshop on Foundations of Object-Oriented Languages.
Submitted to a special issue of Theory and Practice of Object-oriented
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.
CADE-13 Workshop on Proof Search in Type-Theoretic 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 363-381. Springer-Verlag.
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 60-82. Springer-Verlag.
- 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 19-61, LNCS 806, Springer-Verlag
- Healfdene Goguen,
A Typed Operational Semantics for Type Theory,
Abstract, PhD Thesis, LFCS Technical Report ESC-LFCS-94-304
- 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 Alpha-Conversion,
Types for Proofs and Programs: International
Workshop TYPES'93, Nijmegen, May 1993, Selected Papers.
Henk Barendregt and
Tobias Nipkow (editors),
pages 313-332, LNCS 806, Springer-Verlag
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: Well-Ordering Types Revisited.
In G. Huet and
Gordon Plotkin (eds.), Logical Environments,
Cambridge University Press,
1993. Also as
ECS-LFCS-92-209,
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
ECS-LFCS-91-131,
Edinburgh University.
[Click here
for its dvi-file.]
- 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 ECS-LFCS-92-230. 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 ECS-LFCS-92-228
- Rod Burstall and
James McKinna,
Deliverables: A categorical approach to program development in type theory, Introduction, LFCS Technical Report ECS-LFCS-92-24
- 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
ECS-LFCS-92-202,
Edinburgh University.
Univ.
LFCS Technical Report ECS-LFCS-92-202
- Zhaohui Luo and Randy Pollack,
LEGO Proof Development System: User's Manual
, LFCS Technical Report ECS-LFCS-92-211. 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 ECS-LFCS-91-132
- Robert Harper and
Randy Pollack,
Type Checking with Universes
, TCS, Volume 89, pages 107-136
- 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. 209-222.
- 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