ML program with callcc

Article View: comp.lang.functional

Article #1054

Back to comp.lang.functional Previous Next

#1054

From: Martin Hofmann
Date: Wed, 27 Jan 1993 18:31

21 lines
1089 bytes

Hello,

I am interested in the use of type theory for the verification of functional
programs and it is in this context that i'm looking for ml-programs which

make nontrivial use of callcc

and nevertheless do neither use references nor mixed variance datatypes 

the latter means that there are no datatypes like

datatype D=A of int|B of D->D

where the recursively def'd type occurs to the left of an arrow.

Can anybody help?
-- 
                 Martin Hofmann         	
 Laboratory for Foundations of Computer Science 	      	
       The King's Buildings, Mayfield Rd
 Edinburgh EH9 3JZ               Phone 650 5188

Technical Details

Message-ID: <C1IzGA.A6B@dcs.ed.ac.uk>

Path:

arc1-ca.pugleaf.net!sparky!uunet!crdgw1!rpi!uwm.edu!spool.mu.edu!agate!doc.ic.ac.uk!warwick!uknet!edcastle!dcs.ed.ac.uk!mxh

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!sparky!uunet!crdgw1!rpi!uwm.edu!spool.mu.edu!agate!doc.ic.ac.uk!warwick!uknet!edcastle!dcs.ed.ac.uk!mxh
From: mxh@dcs.ed.ac.uk (Martin Hofmann)
Newsgroups: comp.lang.functional
Subject: ML program with callcc
Keywords: continuations
Message-ID: <C1IzGA.A6B@dcs.ed.ac.uk>
Date: 27 Jan 93 18:31:22 GMT
Sender: cnews@dcs.ed.ac.uk (UseNet News Admin)
Organization: Department of Computer Science, University of Edinburgh
Lines: 21