home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / lang / function / 1559 < prev    next >
Encoding:
Internet Message Format  |  1993-01-28  |  1.0 KB
  1. Path: sparky!uunet!crdgw1!rpi!uwm.edu!spool.mu.edu!agate!doc.ic.ac.uk!warwick!uknet!edcastle!dcs.ed.ac.uk!mxh
  2. From: mxh@dcs.ed.ac.uk (Martin Hofmann)
  3. Newsgroups: comp.lang.functional
  4. Subject: ML program with callcc
  5. Keywords: continuations
  6. Message-ID: <C1IzGA.A6B@dcs.ed.ac.uk>
  7. Date: 27 Jan 93 18:31:22 GMT
  8. Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
  9. Organization: Department of Computer Science, University of Edinburgh
  10. Lines: 21
  11.  
  12. Hello,
  13.  
  14. I am interested in the use of type theory for the verification of functional
  15. programs and it is in this context that i'm looking for ml-programs which
  16.  
  17. make nontrivial use of callcc
  18.  
  19. and nevertheless do neither use references nor mixed variance datatypes 
  20.  
  21. the latter means that there are no datatypes like
  22.  
  23. datatype D=A of int|B of D->D
  24.  
  25. where the recursively def'd type occurs to the left of an arrow.
  26.  
  27. Can anybody help?
  28. -- 
  29.                  Martin Hofmann             
  30.  Laboratory for Foundations of Computer Science               
  31.        The King's Buildings, Mayfield Rd
  32.  Edinburgh EH9 3JZ               Phone 650 5188
  33.