Publications of the Programming Logic Group

• 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 Martin-Lö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 machine-assisted proofs: The Integers form an Integral Domain
  Licentiate thesis, 1993.
• Experiences with a mechanisation of Martin-Löf's theory of types (with Eduardo Gimenez)
  Technical report 91-08, Inco, Pedeciba, 1991.

• Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids (with Peter Dybjer)
  Proccedings of TYPES'95, LNCS 1158, pp 47-61.
• A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem (with Sten Agerholm and Peter Dybjer)
  Proceedings of TPHOL'96, LNCS 1125, pp 17-32.

• A Machine-assisted 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 (Latin-American 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.

• A Machine Assisted Proof of the Hahn-Banach Theorem
  To appear, 1997.
• An implementation of the Heine-Borel covering theorem in type theory
  To appear, 1997.
• A Constructive Proof of the Heine-Borel Covering Theorem for Formal Reals (with Sara Negri)
  In S. Berardi and M. Coppo eds., TYPES for Proofs and Programs, LNCS 1158, pp. 62--75, Springer-Verlag, 1996.
• The Hahn-Banach 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.

• From semantics to rules : A machine assisted analysis
  Published in CSL'93, Springer Verlag, LNCS 832.
• A normalization proof for Martin-Löf's type theory
• Combinator Shared Reduction and Infinite Objects in Type Theory

• A constructive topological proof of van der Waerden's theorem
• Minimal spaces in formal topology
• Computational content of classical logic
• A formal space of ultrafilters
• An application of boolean models
• A topos theoretic fixpoint theorem
• Type Theory and Formal Topology (Talk given in Venice, october 1995)
• Minimal Spaces (Talk given in Uppsala, may 1995)
• Formal Topology with Posets
• Infinite Objects in Type Theory (To be updated.)
• Pattern Matching in Type Theory (To be updated.)
• A Formal Space of Paths
• An Algorithm for Type-Checking Dependent Types

• 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 well-orderings in Martin-Lö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 75-94.
• Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids (with Ilya Beylin)
  pp 47-61 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 17-32 in Theorem Proving in Higher Order Logics, editors J. von Wright, J. Grundy, J. Harrison, LNCS 1125, August 1996.
• Internal type theory
  pp 120-134 in TYPES '95, LNCS 1158, 1996.
• A general formulation of simultaneous inductive-recursive 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 440-465.
• Inductive sets and families in Martin-Löf's type theory and their set-theoretic semantics
  Logical Frameworks, 1991, editors Gerard Huet and Gordon Plotkin, pp 280-306, Prentice Hall.

• Higman's lemma in type theory

• A Type-Theoretic Interpretation of Constructive Domain Theory
  Journal of Automated Reasoning 16, 1996, pp 369-425.
• Type theory and the External Logic of Programs
  Dissertation for the Ph. D. Degree in Computing Science, ISBN 91-7032-984-2 CTH, Göteborg 1994.
• Normalizing the Associative Law: An Experiment with Martin Löf's Type Theory
  Formal Aspects of Computing 3, 1991, pp 218-252.

• Martin-Lö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 Martin-Löf's Type Theory (with Kent Petersson and Jan Smith).
  Oxford University Press, 1990.
• Terminating General Recursion
  BIT, Vol. 28, pp. 605-619, 1988.
• Multilevel Functions in Martin-Lö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 Martin-Löf's Type Theory (with Jan Smith)
  BIT, Vol. 24, pp. 288-301, 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.

• Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory
  Licentiate thesis, Oct 1996.
• A Proof-Theoretical Investigation of Zantema's Problem
  Joint work with Thierry Coquand. Presented at CSL'97.

• Beräkningsbarhet för dataloger, Från lambda till P
  Bokförlaget Aquila, 1988.
• Programming in Martin-Lö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 Martin-Lö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.
• Martin-Löf's Type Theory (with Bengt Nordström and Jan M Smith)

• Type theory and Programming (with Thierry Coquand, Bengt Nordström and Jan Smith)
  An introduction to type theory and its applications to programming.
• A user's guide to ALF (with Thorsten Altenkirch, Veronica Gaspes and Bengt Nordström)
  Describes a computer implementation of a logical framework in which many formal systems can be implemented.
• A machine-assisted proof of the fundamental theorem of arithmetic
  Describes an ALF proof in Martin-Löf Set Theory of the theorem of the title.
• Program verification in ALF
  Discusses how functional programs can be verified using the ALF system.
• Dependently typed binomial queues
  Shows by means of an example how dependent types can be useful to express representation invariants in abstract data types.

• Towards a Theory of Specifications, Programs and Proofs (1995)
• A Machine Checked proof that Ackermann's Function is not Primitive Recursive(1991)