Quick overview of my research on gradual typing.
Presented at Utah's CS3020: Undergrad Research Forum.
This is a long introduction before the main event: Reliable Numeric Design for ML via PL.
Part of a series by the Journal of Functional Programming to make PhD
Abstracts available to a wider audience.
Thanks JFP!
Slides from a BU POPV seminar about understanding the design space of languages that mix typed and untyped code.
Worked example of a reduction that gets stuck due to a metafunction under the Transient semantics of Big Types in Little Runtime (POPL 2017).
Bottom line: it's tricky to pinpoint what subterm of a type is at fault when a type-tag check fails.
Jesse Alama wrote a thoughtful survey about language-oriented programming in Racket and collected responses from 30 "seasoned Racket developers" into a book.
I am a respondent.
Quick reference for the git command-line tool.
Covers:
- basic command (add, diff, push)
- how to undo
- the difference between local and shared (remote) repositories
- how to identify and fix basic push & pull errors (e.g., merge conflicts)
This post explains the sampling method introduced in the paper On the Cost of Type-Tag Soundness.
[src]
Type tailoring is a technique for adding domain-specific type
checkers to a typed host language. Using the Type Systems as Macros
approach to building typed languages, implementing type tailoring in
Typed Racket is straightforward. Any library can apply the core idea,
and you can try programming with type tailorings by downloading the
trivial package (requires Racket v6.4 or later).
[src]
The source code for the PRL website is written using Scribble, the Racket documentation tool. I am very happy with this choice, and you should be too!
[src]
Tired of writing (require (for-syntax syntax/parse)) at the
top of your Racket programs? This post shows how to make a #lang to
customize your default programming environment.
[src]
An overview of the IFDS framework for modeling and solving problems in static analysis, following the POPL 1994 paper.
Presented in Frank Tip's CS7480.
Performance matters for software systems, but performance is not always easy to measure. At the PRL we recently had a scare with some unreliable measurements. Here is the story.
[src]
Racket is excellent for incrementally growing scripts into full-fledged programs. This post steps through the evolution of one small program and highlights the Racket tools that enable incremental advances.
[src]
The very basics of Craig Interpolation, presented in Thomas Wahl's CS7485.
Quick summary of Kildall's Algorithm for global static analysis.
May be my favorite fixpoint.
Presented at PL junior.
Brief summary of the seminal work by Plotkin.
Bottom line: languages and calculi must be developed together.
Also it is possible to build (inefficient) order-of-evaluation-independent interpreters; however, a call-by-value language is marginally better for the task.
Presented at PL junior.
A fast walk through the CompCert compiler.
Goes over the architecture, correctness strategy, and correctness proof.
Presented in CS 7480.
Notes and code and references introducting coinduction, mostly through streams.
Presented at Northeastern's PL junior seminar.
A brief overview of logical relations.
Presented at Northeastern's PL junior seminar.