home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #18 / NN_1992_18.iso / spool / comp / archives / 3161 < prev    next >
Encoding:
Internet Message Format  |  1992-08-20  |  4.0 KB
  1. Path: sparky!uunet!elroy.jpl.nasa.gov!ames!agate!agate!usenet
  2. From: kentp@cs.chalmers.se
  3. Newsgroups: comp.archives
  4. Subject: [fj.mail-lists.types] Informal Baastad proceedings by FTP
  5. Followup-To: fj.mail-lists.types
  6. Date: 21 Aug 1992 11:00:32 GMT
  7. Organization: University of California, Berkeley
  8. Lines: 77
  9. Approved: adam@soda.berkeley.edu
  10. Distribution: world
  11. Message-ID: <172icgINNhkk@agate.berkeley.edu>
  12. References: <313934@nttlab.ntt.JP>
  13. NNTP-Posting-Host: soda.berkeley.edu
  14. X-Original-Newsgroups: fj.mail-lists.types
  15. X-Original-Date: 20 Aug 92 19:14:42 GMT
  16.  
  17. Archive-name: auto/fj.mail-lists.types/Informal-Baastad-proceedings-by-FTP
  18.  
  19. Date: Thu, 20 Aug 92 10:37:31 +0200
  20.  
  21. The informal proceedings of the Workshop on Types for Proofs 
  22. and Programs, B\aa stad, Sweden are now available by ftp.
  23.  
  24. In order to be able to LaTeX all documents together I had to change
  25. some things in the papers. I hope I have not destroyed too much.
  26.  
  27. The proceedings can be obtained by anonymous ftp from Chalmers
  28. University of Technology. The compressed file is bastad92/proc.ps.Z on
  29. the machine animal.cs.Chalmers.SE, login name ``anonymous'' and your
  30. ordinary name as password. There is also a 'dvi' file but if you
  31. prefer that you must also take the two files mizar_app_50[56].ps.
  32. (the "official" version is LaTeX'ed for being printed on both sides of
  33. the paper, if you prefer single sided printing use proc.ps.SS.Z
  34. instead)
  35.  
  36. The proceedings contain the following papers:
  37.  
  38.   P. Aczel:         Schematic Consequence    
  39.   P. Audebaud:      CC+ : an extension of the Calculus of
  40.             Constructions with fixpoints
  41.   F. Barbanera:     Continuations and Simple Types: a Strong 
  42.             Normalization Result (abstract)    
  43.   S. Berardi:       Game theory and Program extraction (abstract)    
  44.   R. Burstall,
  45.   James McKinna:    Deliverables: a categorical approach to program 
  46.             development in type theory    
  47.   T. Coquand:       Pattern Matching with Dependent Types    
  48.   C. Coquand:       A proof of normalization for simply typed lambda 
  49.             calculus written in ALF     
  50.   V. Danos,      
  51.   L. Regnier:       Virtual reduction (abstract)    
  52.   J. Despeyroux,
  53.   A. Hirschowitz:   Natural Semantics in Coq. First experiments    
  54.   P. Dybjer:        Universes and a General Notion of Simultaneous 
  55.             Inductive-Recursive Definition in Type Theory    
  56.   D. Fridlender:    Formalizing Properties of Well-Quasi Ordered Sets 
  57.             in  ALF     
  58.   V. Gaspes:        Formal Proofs of Combinatorial Completeness    
  59.   V. Gaspes,      
  60.   J. M. Smith:      Machine Checked Normalization Proofs for Typed
  61.             Combinator Calculi    
  62.   H. Geuvers:       Inductive and Coinductive types with Iteration 
  63.             and Recursion    
  64.   L. Helmink:       Girard's Paradox in lambda U (abstract)    
  65.   H. Herbelin:      Computable interpretation of cross-cuts 
  66.             procedure (abstract)    
  67.   B. Jutting:       Typing in Pure Type Systems (abstract)    
  68.   J. Lipton:        Relating Logic Programming and Propositions-as-Types:
  69.             A Logical Compilation
  70.   F. Leclerc,      
  71.   C. Paulin:        Programming with Streams in Coq. A case study : 
  72.             the Sieve of Eratosthenes    
  73.   Z. Luo:           Compositional understanding of type theory (abstract)    
  74.   L. Magnusson:     The new Implementation of  ALF     
  75.   N. Mendler,      
  76.   P. Aczel:         An implementation of Constructive Set Theory, 
  77.             in the Lego system    
  78.   M. Parigot:       lambda mu-calculus: an algorithmic interpretation 
  79.             of classical natural deduction (abstract)    
  80.   F. Pfenning:      Teaching Theory of Programming Languages Using 
  81.             a Logical Framework: an Experience Report (abstract)    
  82.   D. Pym,      
  83.   G.Plotkin:         A Relevant Analysis of Natural Deduction (abstract)    
  84.   C. Raffalli:       Fixed point and type systems (abstract)    
  85.   P. Rudnicki:       An Overview of the  MIZAR  Project    
  86.   A. K. Simpson:     Kripke Semantics for a Logical Framework    
  87.   B. Werner:         A Normalization Proof for an Impredicative Type 
  88.              System with Large Elimination over Integers    
  89.  
  90.  
  91.     Kent Petersson
  92.     kentp@cs.Chalmers.SE
  93.  
  94.