David Van Horn dvanhorn

dvanhorn / sweet-redex.rkt

Created July 31, 2012 07:34

Sweet notation in Redex

	#lang planet asumu/sweet racket
	require rename-in(redex [term quote])

	define-language lang
	e n
	δ1(e)
	δ2(e e)
	δ1 √ add1 sub1
	δ2 + - * /
	E hole

dvanhorn / parv.rkt

Created July 8, 2012 20:05

Parallel beta-reduction for the call-by-value lambda-calculus

	#lang racket
	(require redex/reduction-semantics)
	;; http://lists.racket-lang.org/users/archive/2012-July/053013.html

	(define-language Λ
	[X variable]
	[V (λ X E)]
	[P E] ; side-condition: closed
	[E (λ X E) (E E) X]
	[F (% (λ X E) F) (λ X E) (F F)])

dvanhorn / par.rkt

Created July 8, 2012 18:12

Parallel beta-reduction for the lambda-calculus

	#lang racket
	(require redex/reduction-semantics)
	;; http://lists.racket-lang.org/users/archive/2012-July/053007.html

	(define-language Λ
	[X variable]
	[E (λ X E) (E E) X]
	[F (% (λ X F) F) (λ X F) (F F) X])

	;; Mark all redexes

dvanhorn / cpcf-machine.rkt

Created July 4, 2012 03:21

Machine semantics for Contract PCF

	#lang typed/racket
	;; Machine semantics for Contract PCF

	;; SYNTAX
	;; ======
	;;
	;; E = (vbl X)
	;; \| (app E E)
	;; \| (if E E E)
	;; \| (lam X E)

dvanhorn / cpcf-den.rkt

Created July 3, 2012 18:32

Denotational semantics for Contract PCF

	#lang typed/racket
	;; Denotational semantics for Contract PCF

	;; SYNTAX
	;; ======
	;;
	;; E = (vbl X)
	;; \| (app E E)
	;; \| (if E E E)
	;; \| (lam X E)

dvanhorn / Evaluator.java

Created October 28, 2011 02:12

Compositional interpreter for lambda calculus as Visitor in Java for @ccshan @djspiewak @kaleidic

	// Compositional evaluator as visitor

	import java.math.BigInteger;

	// Syntax

	interface Exp {
	<X> X accept(Visitor<X> v);
	}

dvanhorn / stack-trace.txt

Created October 28, 2011 01:51

Higher-order programming in Java

	doom:shan dvanhorn$ java Eval
	Exception in thread "main" java.lang.StackOverflowError
	at Evaluate.visit(Eval.java:142)
	at Evaluate.visit(Eval.java:119)
	at App.accept(Eval.java:56)
	at Evaluate.visit(Eval.java:142)
	at Evaluate.visit(Eval.java:119)
	at App.accept(Eval.java:56)
	at Evaluate$1.apply(Eval.java:136)
	at Evaluate.visit(Eval.java:142)

dvanhorn / circular.rkt

Created October 20, 2011 03:00

Circular language

	#lang racket
	(require redex/reduction-semantics)

	(define-language C
	(CON X
	nat?
	(or/c CON CON)
	(rec/c X CON)
	(cons/c CON CON)
	(CON -> CON))

dvanhorn / flat-v-ho.rkt

Created October 20, 2011 02:41

The smart way and the dumb way

	#lang racket
	(require redex/reduction-semantics)

	(define-language pre-C
	(CON X
	nat?
	(or/c CON CON)
	(rec/c X CON)
	(cons/c CON CON)
	(CON -> CON))

dvanhorn / peer.txt

Created October 15, 2011 19:22

The essence of peer review

	diff popl12-reviews.txt popl12-reviews-final.txt
	333c333
	< Updated Tuesday 6 Sep 2011 6:28:00pm EDT
	---
	> Updated Monday 19 Sep 2011 1:03:02pm EDT
	339c339
	< Overall merit: 4. Accept
	---
	> Overall merit: 3. Weak accept
	525d524