home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1993 #3 / NN_1993_3.iso / spool / comp / theory / 2942 < prev    next >
Encoding:
Internet Message Format  |  1993-01-28  |  1.1 KB
  1. Path: sparky!uunet!ukma!usenet.ins.cwru.edu!agate!ames!haven.umd.edu!mimsy!pugh
  2. From: pugh@cs.umd.edu (Bill Pugh)
  3. Newsgroups: comp.theory
  4. Subject: Re: Adding Constraints to Automate Programming
  5. Message-ID: <63817@mimsy.umd.edu>
  6. Date: 28 Jan 93 22:27:48 GMT
  7. References: <BAZET.93Jan27195118@chailly.ensmp.fr>
  8. Sender: news@mimsy.umd.edu
  9. Distribution: comp
  10. Organization: U of Maryland, Dept. of Computer Science, Coll. Pk., MD 20742
  11. Lines: 23
  12.  
  13. In article <BAZET.93Jan27195118@chailly.ensmp.fr> bazet@chailly.ensmp.fr (Philippe BAZET) writes:
  14. >Let us consider a circular list. It can be defined by an ML-like data
  15. >type such as
  16. >
  17. >    list 'a = nil | cons of 'a * list 'a ;
  18. >
  19. >and the assertion:
  20. >
  21. >    The last element for the list is the first one.
  22. >
  23. >Does anyone know of programming systems in which such assertions can be
  24. >expressed formally and used at either run-time or compile-time? 
  25.  
  26. Check out the paper "Graph Types" by Nils Klarlund and Michael Schwartzback
  27. in the 93 POPL conference.
  28.  
  29.     Bill Pugh
  30.     Dept. of Computer Science
  31.     Univ. of Maryland, College Park
  32.     pugh@cs.umd.edu
  33.  
  34.  
  35.  
  36.