mark ippolito
a.k.a. maria ippolito.
any pronouns
about me
I'm a recent graduate with a BSc in Computer Science interested in programming languages, graphics coding, abstract math, linguistics, and HCI.
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
code sample
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)) # final result nums() with (yield n -> ()) # 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 elements using accumulator { let mut s = 0 let res = nums() with (yield n -> s += n) (sum s, result res) }
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.
