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 lambda-calculus into a couple of categorical programming languages. In Peter Dybjer and Randy Pollack, editors, Informal Proceedings of the Joint CLICS-TYPES 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 Type-Theoretic 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 lambda-calculus formalised: Church-Rosser 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. 251-262.
• 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 19-61, LNCS 806, Springer-Verlag.
• 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.), Prentice-Hall, 1994.
• Adriana Compagnoni. Subtyping in F-omega-wedge is decidable. Technical Report ECS-LFCS-94-281, 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, Springer-Verlag, 1994.
• Healfdene Goguen, A Typed Operational Semantics for Type Theory, Abstract, Ph.D. Thesis, LFCS Technical Report ECS-LFCS-94-304.
• Martin Hofmann, Elimination of extensionality in Martin-L{\"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, Springer-Verlag.
• 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 Z-style schemas in UTT. In Types for Proofs and Programs, LNCS 806. Springer-Verlag, 1994.
• Gordon Plotkin, A Semantics for Static Type Inference. Information and Computation, Vol.109, Nos.1--2, pp. 256--299, 1994.
• Pietro di Gianantonio, Furio Honsell, Silvia Liani and Gordon Plotkin, Countable Non-Determinism and Uncountable Limits. In Proceedings of the conference ``CONCUR '94'' on concurrency theory, pp. 130-145. LNCS 836, Springer-Verlag, 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 Alpha-Conversion, Types for Proofs and Programs: International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers. Henk Barendregt and Tobias Nipkow (editors), pp. 313-332, LNCS 806, Springer-Verlag.
• 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 ECS-LFCS-94-308, 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, ECS-LFCS-93-279, 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. 32-67, LNCS 711, Springer-Verlag.
• Adriana B. Compagnoni and Benjamin C. Pierce. Multiple inheritance via intersection types. Technical Report ECS-LFCS-93-275, LFCS, University of Edinburgh, August 1993. Also available as Catholic University Nijmegen computer science technical report 93-18.
• Philippa Gardner, A New Type Theory for Representing Logics. Fourth International Conference on Logic Programming and Automated Reasoning, LNAI 698, Springer-Verlag, 1993.
• Healfdene 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, 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. 143-184, 1993.
• G. Huet and Gordon Plotkin (eds). Logical Environments. Cambridge University Press, 1993.
• Claudio Hermida. Fibrations, Logical Predicates and Indeterminates. Ph.D. thesis, ECS-LFCS-93-277, 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 ECS-LFCS-91-131, 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. 163-179, 1993.
• Christophe Raffalli. Machine deduction. International Workshop TYPES'93, Nijmegen, May 1993, Selected Papers. Henk Barendregt and Tobias Nipkow (eds.), LNCS 806, Springer-Verlag.
• 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 ECS-LFCS-92-230.
• 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, Dept of Computer Science, University of Edinburgh. 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, 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 ECS-LFCS-91-142.
• Robert Harper and Randy Pollack, Type Checking with Universes , TCS, Volume 89, pages 107-136.
• 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-Verlag.

1990

• Zhaohui Luo, Higher-order Calculus and Theory Abstraction. Information and Computation 90(1), 1990.
• Zhaohui Luo, An Extended Calculus of Constructions. Ph.D. thesis, ECS-LFCS-90-118, University of Edinburgh, 1990. Also as Report CST-65-90, 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 higher-order logic. ECS-LFCS-90-121, Dept of Computer Science, University of Edinburgh.

1989

• Zhaohui Luo, ECC, an Extended Calculus of Constructions. LICS 1989.