mark ippolito

programming languages

I've had a longstanding interest in programming languages from both a practical and theoretical standpoint. In particular with linear types and homotopy type theory. I haven't gotten anything to a state I would call finished, but here are two working prototypes.

ofuda

effect yield = type int -> ()
let nums = () -> {
	yield!(1)
	yield!(2)
	yield!(3)
	"done"
}

# first element
@lbl: { nums(); :none }
with (yield n -> break @lbl :some(n))
= :some(1)
# final result
nums() with (yield n -> ())
= "done"
# sum elements
@lbl: (sum 0, result nums())
with (yield n -> lift @lbl resume -> {
	let (sum s, result res) = resume()
	(sum s + n, result res)
})
= (sum 6, result "done")
# sum elements using accumulator
{
	let mut s = 0
	let res = nums()
	with (yield n -> s += n)
	(sum s, result res)
}
= (sum 6, result "done")

A domain-specific language for scripting with effects via delimited continuations. Created with the goal of compiling to Rust's stack coroutines such that it can be interfaced with from external code. I made the type checker following Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism, extended with effect sets on functions. The interpreter is nearly feature complete, however I need to do more work for the transpilation. I'd like to finish this to use it for making patterns in a shmup game, and for playing around with audio coding.

uv

A dependently-typed language taking a more computationally direct approach to Homotopy Type Theory (e.g. quotients rather than higher inductive types, Higher Observational Type Theory rather than Cubical). Currently I have very little implementation work finished. I would like to use this to play around with directed HoTT as a model for compatibility of modules: talking about whether values are compatible in API (via morphisms as functions) or ABI (via morphisms as reinterpretations).

Inspired by a demo on tomasp.net/coeffects, the typechecker can output judgement-style traces.

judgement sample

Apologies that the output currently contains weird line-wrapping behavior. The visually free-floating judgements are direct children of the root rule.

application development

CPSC 310 project

I worked with a classmate to build a system to query datasets of course sections and rooms. We followed project requirements released in parts as we progressed. The entire application is built using TypeScript. I handled query parsing and evaluation, and the web frontend in React, and my partner handled dataset parsing and the server.

tomany

A desktop application I made for parsing linked media from my existing Obsidian notes into a gallery view. Supports searching by tags and work title, and handles dynamic loading of images. Built in Rust using iced, an Elm-like declarative GUI library.

small things

• command-based svg editor (2018)
• geometry dash 2.2 (fake?) editor option generator (2024)
• knotcovers — command line tool to find portals for a knot (2025)