Publications of the Programming Logic Group
Gustavo Betarte

Dependent Record Types, Subtyping and Proof Reutilization
Presented at the workshop on "Subtyping, inheritance and modular
development of proofs", held at Durham, England, 1997.

Extension of MartinLöf's type theory with record types and
subtyping
(with Alvaro Tasistro)
To appear in "25 Years of Constructive Type Theory", Oxford
University Press, 1997.

Formalisation of Systems of Algebras using Dependent Record Types
and Subtyping: An Example
(with Alvaro Tasistro)
In Proceedings of the 7th. Nordic workshop on Programming Theory,
held at Göteborg, Sweden, 1995.

A case study in machineassisted proofs:
The Integers form an Integral Domain
Licentiate thesis, 1993.

Experiences with a mechanisation of MartinLöf's theory of
types
(with Eduardo Gimenez)
Technical report 9108, Inco, Pedeciba, 1991.
Ilya Beylin
Bror Bjerner (To be completed)
Ana Bove

A Machineassisted Proof of the Subject Reduction Property for
a Small Typed Functional Language
(
abstract ,
extended abstract).
Technical Report of the InCo, 1995.

A Confluent Calculus of Macro Expansion and Evaluation
(with L. Arbilla)
In the Proceedings of the conference Lisp and Functional
Programming
'92 (LFP'92), San Francisco, California, USA, June 1992.

A Confluent Calculus of Macro Expansion and Evaluation
(with L. Arbilla)
Technical Report of the InCo. December 1991. Complete version of
the paper presented at LFP'92.

A Semantics of Syntactic Abbreviations using Explicit Substitutions
Technical Report of the ESLAI (LatinAmerican High School of
Computer Science). December 1990.

Design and Implementation of an Interpreter for the Language
TLL(Typed Lambda Language)(with A. Tasistro)
Technical Report of the ESLAI. August 1990.
Jan Cederquist

A Machine Assisted Proof of the HahnBanach Theorem
To appear, 1997.

An implementation of the HeineBorel covering theorem in type
theory
To appear, 1997.

A Constructive Proof of the HeineBorel Covering Theorem for
Formal Reals (with Sara Negri)
In S. Berardi and M. Coppo eds., TYPES for Proofs and Programs,
LNCS 1158, pp. 6275, SpringerVerlag, 1996.

The HahnBanach Theorem in Type Theory
(with Thierry Coquand and Sara Negri)
To appear in the proceedings of Twentyfive years of
Constructive Type Theory , Venice, 1995.

A machine assisted formalization of pointfree topology in type
theory
Chalmers University of Technology and University of Göteborg,
Sweden, Licentiate Thesis, 1994.
Catarina Coquand
Thierry Coquand
Peter Dybjer

Normalization and the Yoneda embedding(with
Djordje Cubric
and Philip Scott)
Manuscript October 1996. Accepted for publication in
Mathematical Structures in Computer Science.

Representing inductively defined sets by wellorderings in
MartinLöf's type theory
To appear in Theoretical Computer Science.

Intuitionistic model constructions and normalization proofs
(with
Thierry Coquand)
Mathematical Structures in Computer Science (1997), vol 7, pp 7594.

Extracting a proof of coherence for monoidal categories from a
formal proof of normalization for monoids
(with Ilya Beylin)
pp 4761 in TYPES '95, LNCS 1158, 1996.

A Comparison of HOL and ALF Formalizations of a Categorical
Coherence Theorem
(with Sten Agerholm and
Ilya Beylin)
pp 1732 in Theorem Proving in Higher Order Logics, editors
J. von Wright, J. Grundy, J. Harrison, LNCS 1125, August 1996.

Internal type theory
pp 120134 in TYPES '95, LNCS 1158, 1996.

A general formulation of simultaneous inductiverecursive definitions in
type theory
Manuscript, May 1994. Accepted for publication in Journal of
Symbolic Logic.

Implementing a category of sets in ALF (with Veronica Gaspes)
Manuscript, 1993.

Inductive Families
Formal Aspects of Computing 6, 1994, pp 440465.

Inductive sets and families in MartinLöf's type theory and their
settheoretic semantics
Logical Frameworks, 1991, editors Gerard Huet and Gordon
Plotkin, pp 280306, Prentice Hall.
Daniel Fridlender
Veronica Gaspes (To be completed)
Thomas Hallgren (To be completed)
Lars Hallnäs (To be completed)
Michael Hedberg

A TypeTheoretic Interpretation of Constructive Domain Theory
Journal of Automated Reasoning 16, 1996, pp 369425.

Type theory and the External Logic of Programs
Dissertation for the Ph. D. Degree in Computing Science,
ISBN 9170329842 CTH, Göteborg 1994.

Normalizing the Associative Law: An Experiment with Martin Löf's
Type Theory
Formal Aspects of Computing 3, 1991, pp 218252.
Bengt Nordström

MartinLöf's Type Theory (with K. Petersson and J.M. Smith)
A chapter in Handbook of Logic in Computer Science, 1994,
(forthcoming).

The ALF proof editor and its proof engine(with Lena Magnusson)
Springer Lecture Notes in Computer Science 806, 1994.

A user's guide to ALF
(with Thorsten Altenkirch, Veronica Gaspes and Björn von Sydow)

Type theory and Programming
(with Thierry Coquand, Jan Smith and Björn von Sydow)
The EATCS bulletin, February 1994.

Programming in MartinLöf's Type Theory
(with Kent Petersson and Jan Smith).
Oxford University Press, 1990.

Terminating General Recursion
BIT, Vol. 28, pp. 605619, 1988.

Multilevel Functions in MartinLöf's Type Theory
Springer Lecture Notes in Computer Science, vol 217, 1985,
Proceedings of a Workshop on Programs as Data Objects in
Copenhagen, October 1985.

Propositions and Specifications of Programs in MartinLöf's
Type Theory
(with Jan Smith)
BIT, Vol. 24, pp. 288301, 1984.

Types and Specifications (with Kent Petersson)
IFIP '83, Paris.

Programming in Constructive Set Theory, Some Examples
ACM Conference on Functional Languages and Computer
Architecture, Portsmouth, Oct 1981.
Henrik Persson
Kent Petersson

Beräkningsbarhet för dataloger,
Från lambda till P
Bokförlaget Aquila, 1988.

Programming in MartinLöf's type theory,
An introduction
(with Bengt Nordström and Jan M Smith)
Oxford University Press, 1990.

Program Derivation in Type Theory:
A Partitioning Problem
(with Jan M Smith)
Computer Languages, vol. 11, No. 3/4, 1986, pp. 161  172.

Concrete Syntax for Data Types in Functional Languages
(with Annika Aasa and Dan Synek)
Proc. of the 1988 ACM Conference on LISP
and Functional Programming, pp. 96  105,
Snowbird, Utah, July 1988.

A Set Constructor for Inductive Sets in MartinLöf's Type
Theory
(with Dan Synek)
Proc. of the 1989 Conference of Category Theory and Computer
Science, Manchester, U.K., September 1989.
LNCS vol 389, pp. 128  141.

MartinLöf's Type Theory
(with Bengt Nordström and Jan M Smith)
Jan Smith (To be completed)
Björn von Sydow
Nora Szasz
Makoto Takeyama (To be completed)
Last modified: Wed Jan 28 13:43:34 1998
by Henrik Persson