dvanhorn

// This is how I would structure this file:
// https://github.com/luisggpina/defunctionalized-CPS-interpreter/blob/master/src/c/lambda/Interpreter.java

// It ends up looking very much like the ML code you'd write
// using the visitor pattern to achieve pattern matching.

// This is just typed on the fly so it's probably got some
// trivial bugs in it.

dvanhorn

#lang racket
(require redex)

;; There are many different semantics for Call-By-Need
;; in the literature.  Some are purely syntactic:
;; they model sharing using `let' and have complicated 
;; notions of evaluation contexts (e.g. Ariola and 
;; Felleisen). Others are heap-based natural semantics
;; (e.g. Launchbury).

dvanhorn

January 16, 2015

Dear University of Maryland community,

Last month, I alerted you that we face budget challenges. The State of
Maryland now anticipates a deficit of about $750M that is projected to
rise to $1B, if no spending adjustments are made.

Last week, the state Department of Budget and Management announced
immediate budget cuts for all state agencies. The cut for the

dvanhorn

type expr =
  | Int of int
  | Plus of expr * expr

let rec step (e : expr) : expr option =
  match e with
    | Int i -> None
    | Plus (Int i, Int j) ->
	Some (Int (i+j))
    | Plus (Int i, e) ->

dvanhorn

#lang racket
;; This program attempts to render the results
;; of classical 0CFA as a reduction relation.

;; 0CFA is the refl, trans closure of:

;; e0 ~> \x.e    e1 ~> v
;; ---------------------
;; (e0 e1) ~> e, x ~> e1

dvanhorn

Keybase proof

I hereby claim:

• I am dvanhorn on github.
• I am dvanhorn (https://keybase.io/dvanhorn) on keybase.
• I have a public key whose fingerprint is B143 1B4E 5F26 AE09 2237 4878 8544 A994 7647 103C

To claim this, I am signing this object:

dvanhorn

;; BSL program (not Racket)

(require 2htdp/image)
(require 2htdp/universe)

(define BALL-RADIUS 30)
(define WIDTH 500)
(define HEIGHT 500)
(define BACKGROUND (empty-scene WIDTH HEIGHT))
(define TOP BALL-RADIUS)

dvanhorn

#lang racket
(struct vbl (x)       #:transparent)
(struct lam (x e)     #:transparent)
(struct app (e0 e1 l) #:transparent)

(struct mt ()    #:transparent)
(struct ap (e k) #:transparent)
(struct fn (v k) #:transparent)

(define (lookup σ x)

dvanhorn

#lang racket
;(require htdp/draw)
(require "pdfdraw.rkt")
(require lang/posn)
(start 200 200)
(draw-circle (make-posn 0 0) 30 'red)
(draw-solid-disk (make-posn 50 50) 30 'blue)
(draw-solid-rect (make-posn 100 50) 30 60 'yellow)
(draw-solid-rect (make-posn 10 150) 30 60 'green)
(clear-circle (make-posn 50 50) 15 'red) ; color is irrelevant

dvanhorn

Progress:
* mono fstar.exe prints usage and then crashes
* mono fstar.exe of a trivial program crashes

$ mono fstar.exe 
fstar [option] infile...
  --help  Display this information
  --verbosity v
  --z3log  Dump a detailed Z3 debugging log to z3.log
  --z3exe  Call z3.exe instead of via the .NET API (implies --logQueries)