Nate Foster
where else to find them
linkedin:nate-foster-935795125
what they talk about
all 6 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski4 editions2022–2026
- POPL4 editions2021–2024
- OOPSLA2 editions2023–2024
all 11 in the filters
on a stage with
all 70 in the filters
who talks about the same things
- Tobias Kappé4 talks
- Eric Hayden Campbell6 talks
- Nadia Polikarpova24 talks
- David Walker15 talks
- Dexter Kozen4 talks
- Peter Sewell14 talks
| title | conference | date |
|---|---|---|
| Weighted NetKAT: A Programming Language For Quantitative Network Verification | PLDI 2026 | 2026-06-15 |
Weighted NetKAT extends NetKAT to be parametric on a semiring and provides both denotational and operational semantics plus a compiler that turns programs into… | ||
| Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet | RPLS 2025 | 2025-06-17 |
Lightweight verification leverages Sail RISC V specs compiled to a Rust model and the Connie verifier to check per‑instruction faithful emulation and execution… | ||
| StacKAT: Infinite State Network Verification | PLDI 2025 | 2025-06-16 |
Defines StacKAT, a packet-language that adds a single variable-size stack payload with push/pop to NetKAT-style programs and proves program equivalence… | ||
| Active Learning of Symbolic NetKAT Automata | PLDI 2025 | 2025-06-16 |
Presents algorithms that learn symbolic NetKAT automata from active queries, proves soundness and termination, and ships a prototype implementation with… | ||
| Computing Precise Control Interface Specifications | OOPSLA 2024 | 2024-10-20 |
Algorithm computes precise control interface specs for data-plane programs by lifting GCL programs, applying quantifier elimination, and using a path-based… | ||
| KATch: A Fast Symbolic Verifier for NetKAT | PLDI 2024 | 2024-06-24 |
KATch implements NetKAT verification in Scala and replaces exhaustive packet enumeration with symbolic packets, BDD-style relations called SPs that are… | ||
| The Network is the Computer: A Programming Language Perspective | POPL 2024 | 2024-01-14 |
Argues that making switches programmable with the P4 language lets operators push filtering, caching and tiny distributed services into the data plane; shows a… | ||
| Formal Abstractions for Packet Scheduling | OOPSLA 2023 | 2023-10-23 |
Formal operational semantics for PIFO trees and a new notion called homomorphic embedding show when one tree can reproduce another’s packet permutations… | ||
| P4Cub: A Little Language for Big Routers | CPP 2023 | 2023-01-16 |
P4Cub is an IR for P4 with a Petr4 front end and a claim of easier mechanized metatheory: it is mechanized in Coq with both large- and small-step semantics and… | ||
| Panel: Next 50 Years of POPL | POPL 2023 | 2023-01-15 |
Panel discussion surveys POPL's past and future with concrete examples and tensions: cites FlashFill and program synthesis, the 1976 abstract interpretation… | ||
| Deep Programmability: A New Lens on Networking | ICFP 2022 | 2022-09-11 |
Argues that networks are becoming deeply programmable end-to-end and shows concrete tools: a high-level DSL NetKAT with formal semantics and a compiler that… | ||
| Business Meeting - PLDI 2022 | PLDI 2022 | 2022-06-13 |
PLDI 2022 reports concrete process changes: a single flat PC of 120 with four area chairs, no full PC meeting, and asynchronous discussion; paper assignment… | ||
| Islaris: Verification of Machine Code Against Authoritative ISA Semantics | PLDI 2022 | 2022-06-13 |
Islaris verifies machine code against authoritative ISA mechanizations by pruning huge Sail models with SMT-backed Isla symbolic execution into compact Isla… | ||
| Legal Calculi | Programming Languages and the Law 2022 (ProLaLa 2022) | 2022-01-16 |
Proposes a concrete middle layer: small, domain-specific legal calculi that compile nontrivially from human-facing DSLs (Orlando for property, Catala for… | ||
| Littleton: An Educational Environment for Property Law | Programming Languages and the Law 2022 (ProLaLa 2022) | 2022-01-16 |
Littleton is an online, web‑deployable environment built on the Orlando legal programming language that actually names and visualizes property interests, adds… | ||
| Dependently-Typed Data Plane Programming | POPL 2022 | 2022-01-16 |
A dependently-typed P4 called pi4 dependently-typed P4 defines heap types and refinement transformers (a “chomp” Brzozowski derivative) to track bit-level… | ||
| Avenir: Managing Data Plane Diversity with Control Plane Synthesis | NSDI ’21 | 2021-04-12 |
Avenir automatically synthesizes control-plane operations to make diverse data planes behave uniformly, proving soundness and completeness and implementing the… | ||
| Petr4: Formal Foundations for P4 Data Planes | POPL 2021 | 2021-01-17 |
Petr4 provides a clean‑slate definitional interpreter and a compact core calculus that models a P4 fragment, validated by running over 750 tests from the P4… | ||
| Welcome | PLMW @ ICFP 2020 | 2020-08-23 |
Welcome notes report concrete scale and logistics: 275 registered attendees from 32 countries on six continents, enabled by moving PLMW online so scholarships… | ||
| Network Verification: Past, Present, and Future | PEPM 2020 | 2020-01-20 |
A program-verification approach targets real router code written in P4: a verifier called p4v translates P4 to guarded commands, uses a small DSL to model… | ||
| NetChain: Scale-Free Sub-RTT Coordination | NSDI '18 | 2018-04-09 |
NetChain moves the replicated coordination KV store into programmable switches (PISA) to cut client-visible latency to about 9.7 microseconds and to push… | ||
| Semi-Oblivious Traffic Engineering: The Road Not Taken | NSDI '18 | 2018-04-09 |
Combines Räcke’s oblivious routing for a static, capacity-aware path set with a centralized LP that dynamically adjusts split ratios; a software framework… | ||
| nothing matches | ||