dvanhorn

Specifying keep rules for your own code is hard, but the really
hard problem is specifying keep rules for the reflection in a 
library that you did not write yourself. Understanding which keep
rules are necessary (and why) when you are not the author of the
code in question is highly non-trivial. We know that the majority
of Android applications are shipped without shrinking and 
optimization, probably due to the difficulty in getting rules 
right. To me, one of the most compelling possible outcomes of this
research would be a tool that does a safe over-approximation of 
the keep rules necessary so that users have an easy way to get 

dvanhorn

How Sports Ate Academic Freedom 
Big-money athletics undermine universities’ core commitments: truth,
discovery and free inquiry.

By Jay M. Smith
April 30, 2018 5:57 p.m. ET 

Citing “levels of corruption” grave enough to threaten the survival of
the sport, Condoleezza Rice and her NCAA-appointed Commission on
College Basketball have proposed reforms that aim to “put the

dvanhorn

(* Frege to Russell to OCaml

 * Gottlob Frege was a philosopher, logician, and mathematician who is
 * widely credited as the father of analytic philoshophy.  Around the
 * turn of the century he wanted to put mathematics on a rigorous
 * foundation.  To do so, he invented a programming language called
 * axiomatic predicate logic.  The basic idea is that you can express
 * set theory in this logic.  Since much of math can be described in
 * terms of set theory, it therefore could be expressed in axiomatic
 * predicate logic.  If this small core logic could be shown to

dvanhorn

#lang racket
(provide get-news cs.PL)

(require xml net/url)
(define cs.PL  "http://export.arxiv.org/rss/cs.PL")

;; get-news : String -> [Listof [List String String String]]
;; Extract news (title, url, authors) from arXiv RSS feed
(define (get-news rss)
  (match (read-xml (get-pure-port (string->url rss)))

dvanhorn

#lang racket
(provide tweet! (struct-out oauth) current-oauth)
(require (only-in racket/random crypto-random-bytes)
         json
         net/url
         (only-in net/uri-codec [uri-unreserved-encode %])
         web-server/stuffers/hmac-sha1
         (only-in net/base64 base64-encode))

;; tweet! : String -> JSON

dvanhorn

How far is your commute? Why do you choose to bike to work instead of driving? Do you own a car?

My bicycle commute from Park View to College Park varies because I have about a dozen different routes that I like to take. If I don't have time constraints, I prefer taking a route that is about 16 miles long and takes me just over an hour. If I need to get to campus quickly, I can take a route that is just shy of 9 miles and can take less than 40 minutes; that's faster than it takes me to go door to door by Metro. Today, I took a nice long 18.4 mile route that went

dvanhorn

===========================================================================
                           PLDI '16 Review #254A
---------------------------------------------------------------------------
Paper #254: Constructive Galois Connections: Taming the Galois Connection
            Framework for Mechanized Metatheory
---------------------------------------------------------------------------

                 Reviewer expertise: Z. Some familiarity
                      Overall merit: C. Weak paper, though I will not fight
                                        strongly against it

dvanhorn

#lang racket
(require (prefix-in r: (only-in racket delay force)))

(define *memo-tables* 
  (make-hasheq))

(struct matt (f table)
  #:property
  prop:procedure 
  (λ (m . xs) (apply memo m xs)))

dvanhorn

interface Exp {
    <A> A visit(ExpVisitor<A> v);
}

interface Val {
    Val apply(Val a);
    Integer n();
}

abstract class AVal implements Val {

dvanhorn

interface Exp {
    <A> A visit(ExpVisitor<A> v);
}

interface Val {
    <A> A visit(ValVisitor<A> v);
}

abstract class Env {
    public Env extend(String x, Val v) {