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