🚀 go-pugleaf

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