[Prev][Next][Index][Thread]
Informal Baastad proceedings by FTP
Date: Thu, 20 Aug 92 10:37:31 +0200
The informal proceedings of the Workshop on Types for Proofs
and Programs, B\aa stad, Sweden are now available by ftp.
In order to be able to LaTeX all documents together I had to change
some things in the papers. I hope I have not destroyed too much.
The proceedings can be obtained by anonymous ftp from Chalmers
University of Technology. The compressed file is bastad92/proc.ps.Z on
the machine animal.cs.Chalmers.SE, login name ``anonymous'' and your
ordinary name as password. There is also a 'dvi' file but if you
prefer that you must also take the two files mizar_app_50[56].ps.
(the "official" version is LaTeX'ed for being printed on both sides of
the paper, if you prefer single sided printing use proc.ps.SS.Z
instead)
The proceedings contain the following papers:
P. Aczel: Schematic Consequence
P. Audebaud: CC+ : an extension of the Calculus of
Constructions with fixpoints
F. Barbanera: Continuations and Simple Types: a Strong
Normalization Result (abstract)
S. Berardi: Game theory and Program extraction (abstract)
R. Burstall,
James McKinna: Deliverables: a categorical approach to program
development in type theory
T. Coquand: Pattern Matching with Dependent Types
C. Coquand: A proof of normalization for simply typed lambda
calculus written in ALF
V. Danos,
L. Regnier: Virtual reduction (abstract)
J. Despeyroux,
A. Hirschowitz: Natural Semantics in Coq. First experiments
P. Dybjer: Universes and a General Notion of Simultaneous
Inductive-Recursive Definition in Type Theory
D. Fridlender: Formalizing Properties of Well-Quasi Ordered Sets
in ALF
V. Gaspes: Formal Proofs of Combinatorial Completeness
V. Gaspes,
J. M. Smith: Machine Checked Normalization Proofs for Typed
Combinator Calculi
H. Geuvers: Inductive and Coinductive types with Iteration
and Recursion
L. Helmink: Girard's Paradox in lambda U (abstract)
H. Herbelin: Computable interpretation of cross-cuts
procedure (abstract)
B. Jutting: Typing in Pure Type Systems (abstract)
J. Lipton: Relating Logic Programming and Propositions-as-Types:
A Logical Compilation
F. Leclerc,
C. Paulin: Programming with Streams in Coq. A case study :
the Sieve of Eratosthenes
Z. Luo: Compositional understanding of type theory (abstract)
L. Magnusson: The new Implementation of ALF
N. Mendler,
P. Aczel: An implementation of Constructive Set Theory,
in the Lego system
M. Parigot: lambda mu-calculus: an algorithmic interpretation
of classical natural deduction (abstract)
F. Pfenning: Teaching Theory of Programming Languages Using
a Logical Framework: an Experience Report (abstract)
D. Pym,
G.Plotkin: A Relevant Analysis of Natural Deduction (abstract)
C. Raffalli: Fixed point and type systems (abstract)
P. Rudnicki: An Overview of the MIZAR Project
A. K. Simpson: Kripke Semantics for a Logical Framework
B. Werner: A Normalization Proof for an Impredicative Type
System with Large Elimination over Integers
Kent Petersson
kentp@cs.Chalmers.SE