https://drcicero.github.io/topics/ Recent content in Topics on My New Hugo Site Hugo en-us https://drcicero.github.io/topics/choreographic/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/choreographic/ ← Back to Home Write a whole distributed system as one script, and let the compiler split it up. A distributed system is normally written as many separate programs, one per participant, which have to agree on a protocol that exists nowhere in the code. Choreographic programming writes the interaction once, as a single program that names every participant, and a compiler projects it onto the individual endpoints. Protocol mismatches and whole classes of deadlock become programs you cannot write in the first place. https://drcicero.github.io/topics/array-programming/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/array-programming/ ← Back to Home Compilers for machine learning: derive and prove what ML frameworks hard-code. Machine learning runs on a small set of operations (multiply these arrays, differentiate this, invert that) that a compiler ought to derive rather than have a human write out by hand. My work gives these transformations a functional foundation, so they can be optimized aggressively and proved correct rather than trusted. Arrays: a normal form for array programs in which partial evaluation and common subexpression elimination become one algorithm (ECOOP'24). https://drcicero.github.io/topics/incremental/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/incremental/ ← Back to Home Compilers that turn plain functional code into computations that redo only what changed. Most programs throw away their own work: change one cell of a matrix or one row of a table, and the whole computation runs again from scratch. Incremental programming derives from an ordinary functional program a second one that maps a change to the input to the corresponding change to the output, reusing everything that was already computed. https://drcicero.github.io/topics/effects-and-types/ Mon, 01 Jan 0001 00:00:00 +0000 https://drcicero.github.io/topics/effects-and-types/ ← Back to Home Notations and type checkers that let programmers write what they mean, and still check it. A type system is a negotiation. The programmer wants to write what they mean; the compiler wants a guarantee it can actually check. Push too hard on the guarantee and the notation turns rigid (effects marshalled one per line, motives spelled out by hand). Push too hard on convenience and the guarantee evaporates.