Computer Science › Specialization
A continuation is the rest of the computation, reified as a function. Rewriting a program in continuation-passing style makes control flow explicit (every call is a tail call, every intermediate result is named), which is exactly the form that compilers, async/await desugaring, generators, and virtual threads use internally.
An LR parser reads input left to right and builds the rightmost derivation in reverse, using a stack and a finite automaton over sets of grammar items to decide between shifting and reducing. Understanding the tables explains where shift/reduce conflicts come from and why yacc, Bison, and their descendants accept the grammars they do.
LLVM turns the M-languages-by-N-targets compiler problem into M plus N by putting a typed, SSA-form intermediate representation in the middle. Frontends emit memory-based IR, a pipeline of analysis and transformation passes (mem2reg first among them) optimizes it, and a backend lowers it to machine code.
System F adds universal quantification over types to the simply typed lambda calculus, so one definition can be used at every type. Because a polymorphic function cannot inspect its type argument, its type alone constrains what it can do ("theorems for free"), which is the theory behind generics in Java, C#, Rust, and Haskell.
Subtyping lets a value of a more specific type stand in for a more general one, and the rule for function types (contravariant in the argument, covariant in the result) decides which generic types may be substituted. Mutable containers must be invariant to stay sound, which is why Java arrays are a historical mistake and why wildcards, Kotlin's in/out, and bounded quantification exist.
Substructural type systems restrict how often a value may be used. Rust's affine types plus the rule "many readers or one writer" give memory safety and data-race freedom with no garbage collector, and the same discipline (linear types) appears in Linear Haskell and in research languages for resources and protocols.
When types may mention values, a type can state a precise specification (a vector of length n, a sorted list) and a program of that type is a proof that the specification holds. Under the Curry-Howard correspondence, implication is the function type, conjunction is the pair type, and universal quantification is the dependent function type, which is how Lean, Coq/Rocq, and Agda double as programming languages and proof assistants.
Abstract interpretation runs a program over a simplified domain (signs, intervals) instead of concrete values, and a Galois connection between the two guarantees that every concrete behavior is covered. Widening forces loops to converge, trading precision for termination, and the result is a sound analysis that can prove the absence of whole classes of runtime errors.
Almost every other analysis and optimization needs to know which memory locations a pointer or reference may refer to. Andersen's inclusion-based analysis solves subset constraints for precision at cubic worst-case cost, Steensgaard's unification-based analysis merges equivalence classes in near-linear time, and context, field, and heap sensitivity decide where on the precision-cost curve a real tool sits.
Symbolic execution runs a program on symbolic inputs, collecting a path condition at every branch and asking an SMT solver whether each path is feasible and what concrete input drives it. Concolic testing mixes concrete and symbolic execution to generate a test for every path it can reach, at the price of path explosion and limited reasoning about loops, memory, and the environment.
Hoare logic breaks down when pointers alias, because any assertion about one cell might be invalidated by a write through another name. Separation logic adds a separating conjunction P * Q, meaning P and Q hold of disjoint parts of the heap, and a frame rule that lets a proof about a small footprint extend to any larger heap; this is the foundation of Infer, VeriFast, Viper, and the RustBelt proof.
A fuzzer feeds a program mutated inputs and watches for crashes. Coverage-guided fuzzers such as AFL and libFuzzer instrument the target, keep every input that reaches new code, and mutate from those, which turns an exponential blind search into an incremental one; combined with sanitizers they find memory-safety bugs in parsers and protocol code at scale.
Types, abstract interpretation, separation logic, symbolic execution, and fuzzing each give a different guarantee at a different cost. This capstone picks a technique for three realistic situations (nullness in a large Java monorepo, a C parser for untrusted input, a controller that must never raise a runtime error) and states for each exactly what is guaranteed and what is not.
The Language Server Protocol turns the editors-times-languages integration problem into editors plus languages by putting analysis behind a JSON-RPC interface. Making that analysis fast enough to run on every keystroke needs error-tolerant parsing and demand-driven, memoized queries with early cutoff, the same idea that underlies modern build systems.
Part of the Computer Science curriculum.
A continuation is the rest of the computation, reified as a function. Rewriting a program in continuation-passing style makes control flow explicit (every call is a tail call, every intermediate result is named), which is exactly the form that compilers, async/await desugaring, generators, and virtual threads use internally.
An LR parser reads input left to right and builds the rightmost derivation in reverse, using a stack and a finite automaton over sets of grammar items to decide between shifting and reducing. Understanding the tables explains where shift/reduce conflicts come from and why yacc, Bison, and their descendants accept the grammars they do.
LLVM turns the M-languages-by-N-targets compiler problem into M plus N by putting a typed, SSA-form intermediate representation in the middle. Frontends emit memory-based IR, a pipeline of analysis and transformation passes (mem2reg first among them) optimizes it, and a backend lowers it to machine code.
System F adds universal quantification over types to the simply typed lambda calculus, so one definition can be used at every type. Because a polymorphic function cannot inspect its type argument, its type alone constrains what it can do ("theorems for free"), which is the theory behind generics in Java, C#, Rust, and Haskell.
Subtyping lets a value of a more specific type stand in for a more general one, and the rule for function types (contravariant in the argument, covariant in the result) decides which generic types may be substituted. Mutable containers must be invariant to stay sound, which is why Java arrays are a historical mistake and why wildcards, Kotlin's in/out, and bounded quantification exist.
Substructural type systems restrict how often a value may be used. Rust's affine types plus the rule "many readers or one writer" give memory safety and data-race freedom with no garbage collector, and the same discipline (linear types) appears in Linear Haskell and in research languages for resources and protocols.
When types may mention values, a type can state a precise specification (a vector of length n, a sorted list) and a program of that type is a proof that the specification holds. Under the Curry-Howard correspondence, implication is the function type, conjunction is the pair type, and universal quantification is the dependent function type, which is how Lean, Coq/Rocq, and Agda double as programming languages and proof assistants.
Abstract interpretation runs a program over a simplified domain (signs, intervals) instead of concrete values, and a Galois connection between the two guarantees that every concrete behavior is covered. Widening forces loops to converge, trading precision for termination, and the result is a sound analysis that can prove the absence of whole classes of runtime errors.
Almost every other analysis and optimization needs to know which memory locations a pointer or reference may refer to. Andersen's inclusion-based analysis solves subset constraints for precision at cubic worst-case cost, Steensgaard's unification-based analysis merges equivalence classes in near-linear time, and context, field, and heap sensitivity decide where on the precision-cost curve a real tool sits.
Symbolic execution runs a program on symbolic inputs, collecting a path condition at every branch and asking an SMT solver whether each path is feasible and what concrete input drives it. Concolic testing mixes concrete and symbolic execution to generate a test for every path it can reach, at the price of path explosion and limited reasoning about loops, memory, and the environment.
Hoare logic breaks down when pointers alias, because any assertion about one cell might be invalidated by a write through another name. Separation logic adds a separating conjunction P * Q, meaning P and Q hold of disjoint parts of the heap, and a frame rule that lets a proof about a small footprint extend to any larger heap; this is the foundation of Infer, VeriFast, Viper, and the RustBelt proof.
A fuzzer feeds a program mutated inputs and watches for crashes. Coverage-guided fuzzers such as AFL and libFuzzer instrument the target, keep every input that reaches new code, and mutate from those, which turns an exponential blind search into an incremental one; combined with sanitizers they find memory-safety bugs in parsers and protocol code at scale.
Types, abstract interpretation, separation logic, symbolic execution, and fuzzing each give a different guarantee at a different cost. This capstone picks a technique for three realistic situations (nullness in a large Java monorepo, a C parser for untrusted input, a controller that must never raise a runtime error) and states for each exactly what is guaranteed and what is not.
The Language Server Protocol turns the editors-times-languages integration problem into editors plus languages by putting analysis behind a JSON-RPC interface. Making that analysis fast enough to run on every keystroke needs error-tolerant parsing and demand-driven, memoized queries with early cutoff, the same idea that underlies modern build systems.