Archives by Category

Adams

• From lambda to mu: Functions as algebraic types
• Hygiene Reconsidered
• Scrap Your Zippers: A Generic Zipper for Heterogeneous Types

Fall2010

• J-Bob
• Concepts in C++
• Programming with Isomorphisms
• Implementation of the Nanopass Framework
• Wild control operators
• Semantics of Homogeneous Language Embeddings
• Kanor: A Declarative Language for Explicit Communication
• An Equivalence-Preserving CPS Translation via Multi-Language Semantics
• Testing specifications of CPU semantics, or, what I did on my summer vacation
• Communication overhead reduction using static analysis
• A Formal Semantics for Data Analysis and Visualization
• Scrap Your Zippers: A Generic Zipper for Heterogeneous Types

Cottam

• A Formal Semantics for Data Analysis and Visualization

Mahajan

• Communication overhead reduction using static analysis

Kuper

• LVars: Lattice-based Data Structures for Deterministic Parallel and Distributed Programming
• Talk Sign-up Meeting / Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars
• A Lattice-Based Approach to Deterministic Parallelism with Shared State
• Monotonic data structures as a guiding principle for deterministic parallel programming
• A Loopy Introduction to Dependence Analysis
• Some pieces of the Rust object system: extension, overriding, and self
• Parametric polymorphism through run-time sealing, or, theorems for low, low prices!
• Testing specifications of CPU semantics, or, what I did on my summer vacation

Ahmed

• An Equivalence-Preserving CPS Translation via Multi-Language Semantics

Holk

• How to Make a Good Research Artifact
• Region-based Memory Management for GPU Programming Languages: Enabling Rich Data Structures on a Spartan Host
• Towards a Parallel CSS Selector Matching Algorithm in Harlan
• GPU Programming in Rust: Implementing High-level Abstractions in a Systems-level Language
• Fast, Safe Message Passing for Rust
• Region-based Memory Management
• Tasks and Communication in Rust
• Kanor: A Declarative Language for Explicit Communication
• Kanor: A Declarative Language for Explicit Communication

Kulkarni

• Semantics of Homogeneous Language Embeddings

Barker

• Wild control operators

Keep

• A Nanopass Framework Tutorial
• Efficient Procedural Records
• Ftypes: structured foreign data access
• Implementation of the Nanopass Framework

James

• Information effects and their categorical models
• Programming with Isomorphisms

Name

• The Connection Machine
• Concepts in C++

Friedman

• Ask me anything!
• J-Bob

Spring2011

• Ftypes: structured foreign data access
• Animatronic kittehs, 3D printers, and rogue game studios, or, Why computer science education should be just-in-time, not just-in-case, and why (epic) failure should always be an option
• Code Contracts in a World of Uncertainty
• Hygiene Reconsidered
• The Connection Machine
• ConceptClang Prototype Update
• Information effects and their categorical models
• Aspects of Parallelism in DSI (1977-1995)
• Parametric polymorphism through run-time sealing, or, theorems for low, low prices!
• Dynamic Inference of Static Types for Ruby
• Modeling Application Memory Behavior at a High Level
• Mags, the C211 autograder
• Kanor: A Declarative Language for Explicit Communication

McKelvey

• Mags, the C211 autograder

Chauhan

• Modeling Application Memory Behavior at a High Level

Perconti

• Dynamic Inference of Static Types for Ruby

Johnson

• Can Reasoning be Taught?
• Aspects of Parallelism in DSI (1977-1995)

Voufo

• ConceptClang: An Implementation of C++ Concepts in Clang
• ConceptClang Prototype Update

Hansen

• OBT Practice Talks
• Towards a Quantitative Cognitive Model of Software Complexity
• Code Contracts in a World of Uncertainty

Byrd

• miniKanren: Challenges and Opportunities
• Will's Second Annual End-of-the-Year Fun Non-PL PL Wonks Talk: StarCraft
• Declarative Parallel Programming
• Animatronic kittehs, 3D printers, and rogue game studios, or, Why computer science education should be just-in-time, not just-in-case, and why (epic) failure should always be an option

Fall2011

• A Loopy Introduction to Dependence Analysis
• Extensible Programming with First-Class Cases
• Can Reasoning be Taught?
• The Lollipop Guild: Linear Logic and Interactive Fiction
• The Little Register Allocator
• Towards a Quantitative Cognitive Model of Software Complexity
• Closure Optimization
• Hygienic Literate Programming: Lessons from ChezWEB
• cKanren: miniKanren with Constraints
• From lambda to mu: Functions as algebraic types
• Combining Denotational and Operational Semantics for Scalable Proof Development
• A Monad for Deterministic Parallelism
• Some pieces of the Rust object system: extension, overriding, and self
• Tasks and Communication in Rust
• ConceptClang: An Implementation of C++ Concepts in Clang

Newton

• Bringing Atomic Memory Operations to a Lazy Language
• A Monad for Deterministic Parallelism

Foltzer

• A Meta-Scheduler for the Par-Monad: Composable Scheduling for the Heterogeneous Cloud
• Combining Denotational and Operational Semantics for Scalable Proof Development

Alvis

• cKanren: miniKanren with Constraints

Hsu

• A Favorite Thing from Dyalog '17
• APL Style Patterns/Anti-patterns: Escaping the Beginner’s Plateau
• Guaranteed Optimizations in a Data Parallel Compiler
• Co-dfns Compiler Architecture
• The Key to a Data Parallel Compiler
• A Few of My Favorite Things: Compilers and APL
• Array Languages for the Uninitiated
• Extending Concurrent Collections
• OBT Practice Talks
• Hygienic Literate Programming: Lessons from ChezWEB

Dybvig

• Closure Optimization

Wang

• A Fresh View at Type Inference
• Towards Structural Version Control
• The Little Register Allocator

Sparks

• Towards a Computational Account of Homotopy Type Theory
• Boxing for Diamonds: Modal logic and its applications
• Linear Logic Is Broken
• The Abstract Art of Modules
• The Lollipop Guild: Linear Logic and Interactive Fiction

Bowman

• Extensible Programming with First-Class Cases

OBT

• OBT Practice Talks

Spring2012

• Will's Second Annual End-of-the-Year Fun Non-PL PL Wonks Talk: StarCraft
• Violating Contracts: The sad state of the CS judicial system
• A Meta-Scheduler for the Par-Monad: Composable Scheduling for the Heterogeneous Cloud
• Writing Interesting Recursive Programs in a (New) Spartan Host
• Introduction to K: An Executable Semantic Framework
• Efficient Procedural Records
• Monotonic data structures as a guiding principle for deterministic parallel programming
• Monads, Arrows, and Applicative Functors
• Region-based Memory Management
• Extending Concurrent Collections
• Declarative Parallel Programming
• Optimizing Unification
• Towards Structural Version Control
• The Abstract Art of Modules
• OBT Practice Talks

Sabry

• A Computer Science Perspective on the Foundations of Quantum Computing
• Conway Games
• OBT Practice Talks

Martens

• OBT Practice Talks

Thornton

• Formalizing the left-chiastic simply-typed lambda calculus, or: What I did last summer
• Optimizing Unification

Swords

• Expressing Contract Monitoring Strategies for Call-by-Value and Call-by-Name Calculi
• An Introduction to Expressing Contracts as Patterns of Communication
• A Type and Effect System for Contract Monitoring
• Contract Flavors and a Hybrid Contract System
• Violating Contracts: The sad state of the CS judicial system
• Monads, Arrows, and Applicative Functors

Blocher

• Introduction to K: An Executable Semantic Framework

Frisz

• Writing Interesting Recursive Programs in a (New) Spartan Host

Owens

• Contract Monitoring as an Effect

Fall2012

• miniKanren: Challenges and Opportunities
• SIGRONAK
• Array Languages for the Uninitiated
• Linear Logic Is Broken
• Contract Flavors and a Hybrid Contract System
• A Nanopass Framework Tutorial
• Some Information About Scala
• A Fresh View at Type Inference
• A Lattice-Based Approach to Deterministic Parallelism with Shared State
• Introduction to Functional Reactive Programming
• Bringing Atomic Memory Operations to a Lazy Language
• Fast, Safe Message Passing for Rust
• Avalanche: A Fine-Grained Flow Graph Model for Irregular Applications on Distributed-Memory Systems
• Contract Monitoring as an Effect

Willcock

• Avalanche: A Fine-Grained Flow Graph Model for Irregular Applications on Distributed-Memory Systems

Amsden

• Type-Directed Editing
• Type-Directed Editing
• Lifting and Flattening of Typed ASTs
• Introduction to Functional Reactive Programming

Todd

• Some Information About Scala

APL

• A Few of My Favorite Things: Compilers and APL
• Array Languages for the Uninitiated

SIGRONAK

• SIGRONAK

Spring2013

• Lifting and Flattening of Typed ASTs
• Compositional and Lightweight Dependent Type Inference for ML
• A Type and Effect System for Contract Monitoring
• Boxing for Diamonds: Modal logic and its applications
• Enhancing work-stealing runtimes with concurrency
• Linear Dependent Types For Differential Privacy
• GPU Programming in Rust: Implementing High-level Abstractions in a Systems-level Language
• Having Fun in a Turing Tarpit
• A case of Study in Language Based Information Flow Security: RDR Language
• Probabilistic programming and equational reasoning
• Formalizing the left-chiastic simply-typed lambda calculus, or: What I did last summer

Shan

• Exact Recursive Probabilistic Programming
• Probabilistic programming and equational reasoning

Hassan

• A case of Study in Language Based Information Flow Security: RDR Language

Hemann

• microKanren
• ICFP 2016 Practice Talks I
• A Reimplementation of microKanren
• Recovering and enhancing miniKanren
• Having Fun in a Turing Tarpit

Gaboardi

• Linear Dependent Types For Differential Privacy

Zakian

• Directed Cubical Sets and Concurrent Types
• Enhancing work-stealing runtimes with concurrency

Jagannathan

• Compositional and Lightweight Dependent Type Inference for ML

PLFest

• Pre-SPLASH PL-Fest

Fall2013

• Pre-SPLASH PL-Fest

LVars

• Talk Sign-up Meeting / Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars

Spring2014

• Modules and Metaprogramming for the ACL2 Theorem Prover
• Probabilistic Programming for the PL researcher
• Verifying Hybrid Systems with Automated Theorem Provers
• A Few of My Favorite Things: Compilers and APL
• Type-Directed Editing
• Reticulated Python: Gradual Typing for Python
• Conway Games
• LVars: Lattice-based Data Structures for Deterministic Parallel and Distributed Programming
• Recovering and enhancing miniKanren
• Towards a Parallel CSS Selector Matching Algorithm in Harlan
• Linear Types: Out of the Ivory Tower and Into the Trenches
• Monotonic References for Gradual Typing
• Towards a Computational Account of Homotopy Type Theory
• Talk Sign-up Meeting / Freeze After Writing: Quasi-Deterministic Parallel Programming with LVars

HoTT

• Towards a Computational Account of Homotopy Type Theory

Siek

• An Introduction to Step-Indexed Logical Relations via Type Safety for STLC + fix
• Monotonic References for Efficient Gradual Typing
• Refined Criteria for Gradual Typing
• The Essence of Closure Conversion
• Monotonic References for Gradual Typing

GradualTyping

• The Holy Grail of Gradual Security
• Gradual Typing in an Open World
• Refined Criteria for Gradual Typing
• Monotonic References for Gradual Typing

Wailes

• Evaluation of Network/Performance Models for Topologically-Aware Load Balancing: I've Never Meta-Metric I Didn't Like
• Graph Partitioning For Fun and Profit
• Introduction to Topologically-Aware Load Balancing
• Linear Types: Out of the Ivory Tower and Into the Trenches

Vitousek

• Big Types in Little Runtime (Open-World Soundness and Collaborative Blame for Gradual Type Systems)
• Gradual Typing in an Open World
• Design and evaluation of gradual typing for Python
• Reticulated Python: Gradual Typing for Python

Loos

• Verifying Hybrid Systems with Automated Theorem Provers

Zinkov

• Composing Inference Algorithms
• Probabilistic Programming for the PL researcher

Eastlund

• Modules and Metaprogramming for the ACL2 Theorem Prover

Security

• The Holy Grail of Gradual Security
• Derailer: Interactive Security Analysis for Web Applications

Near

• Derailer: Interactive Security Analysis for Web Applications

Fall2014

• The Essence of Closure Conversion
• A Combinator Library for MCMC Sampling
• An Introduction to Dependently Typed Racket
• MACE: Detecting Privilege Escalation Vulnerabilities in Web Applications
• Pycket: an implementation of Racket in RPython
• A Compiler for the Gradually-Typed Lambda Calculus
• Design and evaluation of gradual typing for Python
• Region-based Memory Management for GPU Programming Languages: Enabling Rich Data Structures on a Spartan Host
• A Method for Proving Congruence of Bisimilarity in Nominal SOS
• Type-Directed Editing
• Introduction to Topologically-Aware Load Balancing
• Typed Clojure in Practice
• Derailer: Interactive Security Analysis for Web Applications

Bonnaire-Sergeant

• Space-Efficient Runtime Tracking
• Automatically generating clojure.spec annotations
• Hash Array Mapped Tries
• Practical Optional Types for Clojure
• Typed Clojure: From Optional to Gradual Typing
• Running Typed Racket Backwards
• Typed Clojure in Practice

Clojure

• Typed Clojure in Practice

Cimini

• Well-Typed Languages are Sound
• A methodology, conceptual procedures and a supporting tool for Gradual Typing
• A Method for Proving Congruence of Bisimilarity in Nominal SOS

Kuhlenschmidt

• A Novice's Quick Plunge into Coq!
• Toward Absolutely Efficient Gradual Typing
• A Compiler for the Gradually-Typed Lambda Calculus

Bauman

• Pycket: an implementation of Racket in RPython

Naldurg

• MACE: Detecting Privilege Escalation Vulnerabilities in Web Applications

Kent

• Pony: A Brief Programming Language Overview!
• Type Checker Tune-up
• Two PLDI Practice Talks (see description)
• PLT Redex Tutorial @ Wonks
• Status Report: Enriching Typed Racket with Dependent Types
• An Introduction to Dependently Typed Racket

Narayanan

• Symbolic conditioning of arrays in probabilistic programs
• Probabilistic Programming in Hakaru
• A Combinator Library for MCMC Sampling

Contracts

• An Introduction to Expressing Contracts as Patterns of Communication
• Verification and Refutation of Behavioral Contracts with Higher-Order Symbolic Execution

VanHorn

• Verification and Refutation of Behavioral Contracts with Higher-Order Symbolic Execution

Spring2015

• Ask me anything!
• Toward Absolutely Efficient Gradual Typing
• Status Report: Enriching Typed Racket with Dependent Types
• Adaptively Scalable Data Structures
• Monotonic References for Efficient Gradual Typing
• An Introduction to Expressing Contracts as Patterns of Communication
• Chiastic Lambda-Calculi
• Running Typed Racket Backwards
• Directed Cubical Sets and Concurrent Types
• The Key to a Data Parallel Compiler
• How to Make a Good Research Artifact
• Refined Criteria for Gradual Typing
• Semester Organizational Meeting
• Verification and Refutation of Behavioral Contracts with Higher-Order Symbolic Execution

Organizational

• Semester Organizational Meeting
• Semester Organizational Meeting
• Semester Organizational Meeting
• Semester Organizational Meeting
• Semester Organizational Meeting

Romano

• Strong Normalization for Chiastic Lambda-Calculi
• Chiastic Lambda-Calculi

Monotonic

• Monotonic References for Efficient Gradual Typing

Gradual

• The Holy Grail of Gradual Security
• Toward Absolutely Efficient Gradual Typing
• Monotonic References for Efficient Gradual Typing

Fogg

• Adaptively Scalable Data Structures

DataStructures

• Adaptively Scalable Data Structures

Haskell

• Generic Programming for the Masses
• Unboxing Sum Types in GHC
• Adaptively Scalable Data Structures

Racket

• PLT Redex Tutorial @ Wonks
• Status Report: Enriching Typed Racket with Dependent Types

Types

• Status Report: Enriching Typed Racket with Dependent Types

GradualTypes

• The Holy Grail of Gradual Security
• Toward Absolutely Efficient Gradual Typing

AMA

• Ask me anything!

Practice

• PL-Wonks Workshop: Rehearsal for ICFP, FHPC, HIW, Haskell symposium, Scheme workshop, LCPC

Talks

• PL-Wonks Workshop: Rehearsal for ICFP, FHPC, HIW, Haskell symposium, Scheme workshop, LCPC

ICFP

• PL-Wonks Workshop: Rehearsal for ICFP, FHPC, HIW, Haskell symposium, Scheme workshop, LCPC

Fall2015

• Introduction to Reversible Computing
• Graph Partitioning For Fun and Profit
• Drag
• Gradual Typing in an Open World
• Composing Inference Algorithms
• Fizz and Fuse Your Arrays
• Probabilistic Programming in Hakaru
• Rethinking Loops as Infinite State Transducers
• A methodology, conceptual procedures and a supporting tool for Gradual Typing
• Typed Clojure: From Optional to Gradual Typing
• Semester Organizational Meeting
• PL-Wonks Workshop: Rehearsal for ICFP, FHPC, HIW, Haskell symposium, Scheme workshop, LCPC

Shah

• Rethinking Loops as Infinite State Transducers

Transducers

• Rethinking Loops as Infinite State Transducers

Probabilistic

• Composing Inference Algorithms
• Probabilistic Programming in Hakaru

Vollmer

• Purely Functional GPU Programming
• Fizz and Fuse Your Arrays

Array

• Fizz and Fuse Your Arrays

Optimization

• Fizz and Fuse Your Arrays

Ma

• Drag

Carter

• Cats. We'll talk about cats. (PL Foundations cohort!)
• Category theory in Agda
• Nominal Algebra
• Introduction to Reversible Computing

Reversible

• Introduction to Reversible Computing

Spring2016

• Two PLDI Practice Talks (see description)
• Pycket Using Racket Bytecode
• Expressing Contract Monitoring Strategies for Call-by-Value and Call-by-Name Calculi
• Purely Functional GPU Programming
• Co-dfns Compiler Architecture
• Practical Optional Types for Clojure
• A Reimplementation of microKanren
• Strong Normalization for Chiastic Lambda-Calculi
• Generic Programming for the Masses
• An Introduction to Model Theory
• Unboxing Sum Types in GHC
• Reflecting the Idris Elaborator
• PLT Redex Tutorial @ Wonks
• Semester Organizational Meeting

Redex

• PLT Redex Tutorial @ Wonks

Christiansen

• Felt: Multilingual Literate Racket Programming Without Weaving
• Normalization by Evaluation
• An LCF-Style Tactic Language in Racket's Macro Expander
• ICFP 2016 Practice Talks I
• Reflecting the Idris Elaborator

Idris

• Reflecting the Idris Elaborator

Agacan

• Unboxing Sum Types in GHC

Lewis

• Cats. We'll talk about cats. (PL Foundations cohort!)
• Realizability Models and Logical Relations
• An Introduction to Model Theory

Scott

• Monadic Composition for Deterministic, Parallel Batch Processing
• Detflow: towards deterministic workflows on your favorite OS
• Verified instances for parallel functional programming
• Generic Programming for the Masses

minikanren

• A Reimplementation of microKanren

Derici

• Pycket Using Racket Bytecode

Pycket

• Pycket Using Racket Bytecode

Chamith

• Two PLDI Practice Talks (see description)

Fall2016

• Big Types in Little Runtime (Open-World Soundness and Collaborative Blame for Gradual Type Systems)
• Verified instances for parallel functional programming
• Optimizing first class environments
• microKanren
• Nominal Algebra
• Well-Typed Languages are Sound
• Realizability Models and Logical Relations
• Towards a Theory of Objects in Sequentially Constructive Synchronous Programming
• ICFP 2016 Practice Talks II
• ICFP 2016 Practice Talks I
• Semester Organizational Meeting

McDonell

• ICFP 2016 Practice Talks II

Ismael

• ICFP 2016 Practice Talks II

Mendler

• Towards a Theory of Objects in Sequentially Constructive Synchronous Programming

Walia

• Building high performance DSL's in Racket
• Optimizing first class environments

Spring2017

• Evaluation of Network/Performance Models for Topologically-Aware Load Balancing: I've Never Meta-Metric I Didn't Like
• A Novice's Quick Plunge into Coq!
• Cats. We'll talk about cats. (PL Foundations cohort!)
• Automatically generating clojure.spec annotations
• An LCF-Style Tactic Language in Racket's Macro Expander
• Detflow: towards deterministic workflows on your favorite OS
• Category theory in Agda
• Guaranteed Optimizations in a Data Parallel Compiler
• Type Checker Tune-up
• Hash Array Mapped Tries
• Semester Organizational Meeting

Choudhury

• Homotopy theoretic aspects of Reversible Computing
• Cats. We'll talk about cats. (PL Foundations cohort!)

Fall2017

• Futures in Racket; now and tomorrow
• Felt: Multilingual Literate Racket Programming Without Weaving
• Building high performance DSL's in Racket
• A Favorite Thing from Dyalog '17
• Pony: A Brief Programming Language Overview!
• Midwest Programming Languages Summit
• Monadic Composition for Deterministic, Parallel Batch Processing
• Normalization by Evaluation
• Fall 2017 Recap
• Space-Efficient Runtime Tracking
• Homotopy theoretic aspects of Reversible Computing
• APL Style Patterns/Anti-patterns: Escaping the Beginner’s Plateau
• Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping
• Symbolic conditioning of arrays in probabilistic programs

Chen

• The Holy Grail of Gradual Security
• Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping

Recap

• Fall 2017 Recap

MWPLS

• Midwest Programming Languages Summit

Spall

• Futures in Racket; now and tomorrow

Koronkevich

• One Weird Trick to Untie Landin's Knot

Fall2023

• Exact Recursive Probabilistic Programming
• Universe Hierarchies and (Generalized) Universe Polymorphism
• An Introduction to Step-Indexed Logical Relations via Type Safety for STLC + fix
• One Weird Trick to Untie Landin's Knot

Angiuli

• Indexed Families in Category Theory, Part III
• Indexed Families in Category Theory, Part II
• Indexed Families in Category Theory
• Universe Hierarchies and (Generalized) Universe Polymorphism

Spring2024

• Sheaves for Process Composition and Separation Logic
• A Computer Science Perspective on the Foundations of Quantum Computing
• Tensor Implementations in Malt (A Deep Learning Toolkit)
• Rhombus, a New Racket Language Without Parentheses
• The Holy Grail of Gradual Security

Tobin-Hochstadt

• Rhombus, a New Racket Language Without Parentheses

Shetty

• Tensor Implementations in Malt (A Deep Learning Toolkit)

VanStarkenburg

• Sheaves for Process Composition and Separation Logic

CategoryTheory

• Sheaves for Process Composition and Separation Logic

SeparationLogic

• Sheaves for Process Composition and Separation Logic

Semantics

• Sheaves for Process Composition and Separation Logic

Fall2024

• Indexed Families in Category Theory, Part III
• Indexed Families in Category Theory, Part II
• Indexed Families in Category Theory

Uskuplu

• Formalizing locally nameless syntax with cofinite quantification

Spring2025

• Lightning talks
• Formalizing locally nameless syntax with cofinite quantification

Germane

• Analyzing Control Flow More Like a Human

Summer2025

• Analyzing Control Flow More Like a Human

Crotts

• How to Design Loops

Fall2025

• How to Design Loops