maria ippolito
a.k.a. mark ippolito.
any pronouns
about me
I'm an undergraduate student in Computer Science at the University of British Columbia interested in programming languages and type theory, Unicode, the semantic web, and accessibility.
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.
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).