dvanhorn

#lang racket
(define in "...")

(define rules
  (list
   (cons "byr" (λ (x) (let ((y (string->number x))) (and y (<= 1920 y 2002)))))
   (cons "iyr" (λ (x) (let ((y (string->number x))) (and y (<= 2010 y 2020)))))
   (cons "eyr" (λ (x) (let ((y (string->number x))) (and y (<= 2020 y 2030)))))
   (cons "hgt" (λ (x) (let ((y (string-length x)))
                        (and (<= 3 y)

dvanhorn

#lang racket
(provide (all-defined-out))
(require redex/reduction-semantics)

;; Redex model of Achieving Safety Incrementally with Checked C, 
;; by Ruef, Lampropoulos, Sweet, Tarditi, & Hicks, POST'19.
;; http://www.cs.umd.edu/~mwh/papers/checkedc-incr.pdf

;; This is written in a monolithic-style where there is a single judgment
;; "⊢" that takes a relation name and input and ouput (in order to be

dvanhorn

#lang racket
(define in "...")

(define (string-ref-mod xs i)
  (string-ref xs (modulo i (string-length xs))))

(define lines (call-with-input-string in port->lines))

(define (c δx δy)
  (for/sum ([x (in-range 0 +inf.0 δx)]

dvanhorn

#lang racket
(define in "...")

(count (λ (x)
         (match (regexp-match #rx"([0-9]*)-([0-9]*) ([a-z]): (.*)" x)
           [(list _
                  (app string->number low)
                  (app string->number high)
                  (app string->list (list a))
                  (app string->list cs))

dvanhorn

#lang racket
;; Redex model of Achieving Safety Incrementally with Checked C, 
;; by Ruef, Lampropoulos, Sweet, Tarditi, & Hicks, POST'19.
;; http://www.cs.umd.edu/~mwh/papers/checkedc-incr.pdf

(provide (all-defined-out))
(require redex/reduction-semantics)

(define *D* (make-parameter (term ()))) ; struct table
(define *H* (make-parameter (term ()))) ; global heap (for type system)

dvanhorn

#lang racket
(define in '(...))
(for*/first ([i (in-list in)]
             [j (in-list in)]
             [k (in-list in)]
             #:when (= (+ i j k) 2020))
  (* i j k))
  

dvanhorn

#lang racket

;; A CPS interpreter for a CBV language written in syntax-rules

;; e ::= 'd                  literal
;;    |  x                   variable
;;    |  (e e ...)           application
;;    |  (λ (x ...) e)       abstraction
;;    |  (let ((x e) ...) e) let
;;    |  (if e e e)          conditional

dvanhorn

#lang racket

;; A CPS interpreter for a CBV language written in syntax-rules

;; e ::= 'd          literal
;;    |  x           variable
;;    |  (e e)       application
;;    |  (λ (x) e)   abstraction

;; (eval e) interprets e in an environment

dvanhorn

#lang racket

;; A CPS interpreter for a CBV language written in syntax-rules

;; e ::= 'd          literal
;;    |  x           variable
;;    |  (e e)       application
;;    |  (λ (x) e)   abstraction

;; (eval e) interprets e in an environment

dvanhorn

#lang racket
(require redex)

;; Run to explore all of the gradual typings of the example
(define (main)
  (traces -> (term example)))

(define-term example
  (λ (x : ?)
    (λ (y : ?)