Darius Foo

A collection of equations

$$\begin{aligned} \mathit{Total\ Correctness} = \mathit{Partial\ Correctness} + \mathit{Termination} \end{aligned}$$
Program Verification

$$\begin{aligned} \mathit{Emacs} + \mathit{Go} = \mathit{Parametric\ Polymorphism} \end{aligned}$$
Fulfilling a Pikedream: the ups of downs of porting 50k lines of C++ to Go.

$$\begin{aligned} \mathit{Product} = \mathit{Customer} \times \mathit{Business} \times \mathit{Technology} \end{aligned}$$
What is a Product?

$$\begin{aligned} \mathit{Algorithm} = \mathit{Logic} + \mathit{Control} \end{aligned}$$
Algorithm = Logic + Control

$$\begin{aligned} \mathit{Cost\ of\ Delay} = & \mathit{User-Business\ Value} + \mathit{Time\ Criticality}\ +\\ & \mathit{Risk\ Reduction\ and}/\mathit{or\ Opportunity\ Enablement} \end{aligned}$$
WSJF - Scaled Agile Framework

$$\begin{aligned} \mathit{Well}\ \text{-}\mathit{founded\ Semantics} + \mathit{Branch\ and\ Bound} = \mathit{Stable\ Models} \end{aligned}$$
Well-founded Semantics + Branch and Bound = Stable Models

$$\begin{aligned} \mathit{Property\ Tests} + \mathit{Contracts} = \mathit{Integration\ Tests} \end{aligned}$$
Property Tests + Contracts = Integration Tests

$$\begin{aligned} \mathit{Compiler}(\mathit{Program}) = \mathit{Algorithms} + \mathit{Data\ Structures} \end{aligned}$$
Next-Paradigm Programming Languages (Wirth)

$$\begin{aligned} \mathit{Clingo} = \mathit{ASP} + \mathit{Control} \end{aligned}$$
Clingo = ASP + Control : Preliminary Report

$$\begin{aligned} \mathit{Assets} = \mathit{Liabilities} + \mathit{Equity} \end{aligned}$$
Balance Sheet - Definition & Examples

$$\begin{aligned} \mathit{Programming} = \mathit{Structure} + \mathit{Efficiency} \end{aligned}$$
What is the use of Continuation Passing Style (CPS)?

$$\begin{aligned} \mathit{Screen} + \mathit{Camera} = \mathit{World} \end{aligned}$$
How to use the SDL viewport properly?

$$\begin{aligned} \mathit{What} + \mathit{When} = \mathit{How} \end{aligned}$$
The Timelines Approach to Consistency in Networked Games

$$\begin{aligned} \mathit{Successful\ Fiction\ Writing} = \mathit{Organizing} + \mathit{Creating} + \mathit{Marketing} \end{aligned}$$
How To Write A Novel Using The Snowflake Method

$$\begin{aligned} \mathit{Model\ Theory} & = \mathit{Universal\ Algebra} + \mathit{Logic} \\ & = \mathit{Algebraic\ Geometry} - \mathit{Fields} \end{aligned}$$
Model theory - Wikipedia

$$\begin{aligned} \mathit{Demonic} + \mathit{Angelic\ Behaviour} = \mathit{Simulation\ Properties} \end{aligned}$$
Deductive Verification with Ghost Monitors

$$\begin{aligned} \mathit{Dynamic\ Scope} + \mathit{Laziness} = \mathit{Counterfactuals} \end{aligned}$$
Dynamic Scope + Laziness = Counterfactuals

$$\begin{aligned} \mathit{Safety} = \mathit{Progress} + \mathit{Preservation} \end{aligned}$$
Types and Programming Languages, Section 8.3

$$\begin{aligned} \mathit{Money} \mathrel{+}= \mathit{Income} - \mathit{Spending} \end{aligned}$$
Retire at 35

$$\begin{aligned} \mathit{Suffering} = \mathit{Pain} \times \mathit{Resistance} \end{aligned}$$
Suffering = Pain x Resistance

$$\begin{aligned} \mathit{Separation\ Logic} + \mathit{Superposition\ Calculus} = \mathit{Heap\ Theorem\ Prover} \end{aligned}$$
Separation Logic + Superposition Calculus = Heap Theorem Prover

$$\begin{aligned} \mathit{Constraint\ Program} = \mathit{Model} + \mathit{Search} \end{aligned}$$
Constraint Programming

$$\begin{aligned} \mathit{Types} + \mathit{Values} & = \mathit{Dependent\ Types} \\ & = \mathit{Types\ Refined\ with\ predicates\ over\ values} \end{aligned}$$
Liquid Types

$$\begin{aligned} \mathit{Pitch\ Pipe} + \mathit{Piano} = \mathit{Pocket\ Pitch} \end{aligned}$$
Pocket Pitch

$$\begin{aligned} \mathit{Refinement\ Types} = \mathit{Types} + \mathit{Logical\ Predicates} \end{aligned}$$
Programming with Refinement Types

$$\begin{aligned} \mathit{Programming} = \mathit{Algorithms} + \mathit{Coding} \end{aligned}$$
PlusCal Tutorial

$$\begin{aligned} \mathit{SAT} + \mathit{Theory\ Solvers} = \mathit{SMT} \end{aligned}$$
First Order Logic (FOL) and Satisfiability Modulo Theories (SMT)

$$\begin{aligned} \mathit{GADTs} = \mathit{Algebraic\ Datatypes} + \mathit{Existential\ Types} + \mathit{Equality\ Constraints} \end{aligned}$$
Polymorphic recursion in OCaml: return values

$$\begin{aligned} \mathit{Hoare\ triples} + \mathit{Monadic\ types} = \mathit{Hoare\ Type\ Theory} \end{aligned}$$
Verification of Imperative Programs in Hoare Type Theory

$$\begin{aligned} \mathit{DSL\ design} = \mathit{Art} + \mathit{Lots\ of\ iterations} \end{aligned}$$
FlashMeta: A Framework for Inductive Program Synthesis

$$\begin{aligned} \mathit{Inverse\ Semantics} + \mathit{Skolemization} = \mathit{Witness\ Function} \end{aligned}$$
FlashMeta: A Framework for Inductive Program Synthesis

$$\begin{aligned} k\text{-}\mathit{FAIR} = k\text{-}\mathit{LIVENESS} + \mathit{FAIR} \end{aligned}$$
Revisiting SAT-based Liveness Algorithms

$$\begin{aligned} \mathit{Cyclic\ proof} = \mathit{pre}\text{-}\mathit{proof}\ \mathcal{P} + \mathit{soundness\ condition}\ \mathcal{S}(\mathcal{P}) \end{aligned}$$
An introduction to cyclic proof

$$\begin{aligned} \mathit{coinduction} = \mathit{use\ of\ finality\ for\ coalgebras} \end{aligned}$$
A Tutorial on (Co)Algebras and (Co)Induction

$$\begin{aligned} \mathit{Query} = \mathit{operation} + \mathit{pattern} \end{aligned}$$
Adaptable Traces for Program Explanations