# 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

### Mahajan

### 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

### 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

### Barker

### Keep

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

### James

### Name

### Friedman

### 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

### Chauhan

### Perconti

### Johnson

### Voufo

### 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

### Foltzer

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

### Alvis

### 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

### Wang

### 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

### OBT

### 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

### 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

### Frisz

### Owens

### 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

### Amsden

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

### Todd

### APL

### 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

### Hassan

### Hemann

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

### Gaboardi

### Zakian

### Jagannathan

### PLFest

### Fall2013

### 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

### 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

### Zinkov

### Eastlund

### Security

### Near

### 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

### 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

### Naldurg

### 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

### 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

### Monotonic

### Gradual

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

### Fogg

### DataStructures

### Haskell

### Racket

### Types

### GradualTypes

### AMA

### Practice

### Talks

### ICFP

### 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

### Transducers

### Probabilistic

### Vollmer

### Array

### Optimization

### Ma

### Carter

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

### Reversible

### 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

### 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

### Agacan

### 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

### Derici

### Pycket

### Chamith

### 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

### Ismael

### Mendler

### Walia

### 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

### MWPLS

### Spall

### Koronkevich

### 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

### 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