L4 formalizations of Hvitved's examples

[Dustin Wehr]

For example, those in Figures 1.1, 1.2, 1.3 (pgs 5-6).

Am I missing something, or does the CSL formalization of Figure 1.1 in Figure 2.3 (pg 42) have the peculiar property that the buyer can force the seller to pay them the full refund of 200 between the buyer's payments of the first and second instalments of 100? 

[Dustin Wehr]

I intended to ask a question; are such formalizations online somewhere?

[Wong Meng Weng]

For CSL, a Haskell implementation (as part of POETS) does exist.

You can see actual working CSL code at https://github.com/legalese/poets/blob/master/usecases/muERP/contracts/Purchase.csl (this repo is our fork of the original code)

If you want to try to get it working on your system, you will find instructions at

https://github.com/legalese/legalese-compiler/tree/master/nix

I have to warn you that after installing POETS on my system I did try running a few CSL programs through the REPL. They worked. But when I tried running a more complex contract of my own devising I discovered an apparent bug in the interpreter, to do with internal choice. Or maybe I just didn't understand CSL correctly and my contract was not very well formed. I don't know. But I gave up at that point with the takeaway that there is some good work here and we should definitely think about using some evolution of CSL / FormaLex as the core of L4.

I haven't looked at your alleged bug yet – but I do wish we could just ask ask a model checker for the answer!

--
You received this message because you are subscribed to the Google Groups "Legalese talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to talk+unsubscribe@lists.legalese.com.
To post to this group, send email to ta...@lists.legalese.com.

--

colle...@legalese.com is a group email address used to provide continuity over multiple individuals.

This message was sent by meng...@legalese.com (Meng Weng Wong) on behalf of Legalese.