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.

a list of datasets loaded into the application
list view
a query on one of the datasets for classes taught by an instructor, sorted by year
search view

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.

tomany example search images from “also saw some intense pigeons” images from “Untitled (Sayaka and Kyouko figures)” images from “一人三女神 (one person, three goddesses)” images from “短くて可愛い (short and cute)” images from “釣り (fishing)” images from “雨季 (rainy season)”
(click on individual images for their sources)

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))
= :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).

small things

some websites i like

  • 1Lab by Amélia Liao et. al
  • takorii.com by takorii
  • Suricrasia Online by blackle mori
  • angusnicneven.com by Angus Nicneven