David Van Horn

One challenge the article omits is that of handling behavioral values such as first-class functions. This is addressed in the following papers: * Higher-Order Symbolic Execution via Contracts. Sam Tobin-Hochstadt...

Package source: Single line text box accepts multi-line input

3

This is a bug that bit some of my students who were trying to install our course software which is distributed as a package on github. In DrRacket, the File...

The scribble/comment-reader causes quasiquote (#\u60) to be replaced by a left single quotation mark (#\u2018), which is inconsistent with what other comment forms produce. For example, the first two produce...

The `racketblock` (and related) form(s) recognize `(code:quote datum)` and typesets it as `(quote datum)`, i.e. without using `'`. There doesn't seem to be a way to do something similar for...

Shouldn't books have titles?

6

Shouldn't there be a title argument? ``` (book-location [#:edition edition #:publisher publisher]) → element? edition : any/c = #f publisher : any/c = #f ```

define-extended-judgment-form should replace rules with same name

1

I was surprised to discover that `define-extended-judgment-form` does not do something similar to `extend-reduction-relation` when an extension names a rule the same as the underlying relation, i.e. replace that rule...

Why is this curried function unsafe?

3

``` #lang racket (require soft-contract/fake-contract) (define ((g x) y) 0) (provide/contract [g (->i ([x (>=/c 0)]) [res () (->i ([y (>=/c 0)]) [res () any/c])])]) ``` I don't understand the...

Soundness bug: fact 4 >= 120

2

This program is incorrectly proved safe. ``` (module factorial racket (define (fact x) (if (zero? x) 1 (* x (fact (sub1 x))))) (provide (contract-out [fact (-> (and/c integer? (>=/c 4))...

Pete Manolios has a paper on random testing that includes a hash function example. Please dig it up and let's see how our system does on it.

Please pull any examples from the QuickCheck paper and add them to the evaluation collection.