Hazel Rose Levine

no longer FDA approved

I’m a third-year undergrad at IU Bloomington, studying pure mathematics and computer science. I use they/them pronouns.

I’m interested in the intersection of programming language theory, human-computer interaction, and computing education. Specifically, I’m very interested in language design, and how advancements in programming languages can change the way users interact with said languages, mapping closer to what a human actually wants to do.

I’m also very interested in type theory (especially homotopy type theory), formal verification, proof theory, and property testing, on the merit that I believe these approaches have potential to further both verification of computer software and verification of mathematical theorems.

I’m currently spending the summer at the University of Minnesota, working on new interaction methods for the cooltt proof assistant.

Projects

  • Bingus, a program synthesizer for code as found in the How to Design Programs textbook, to help facilitate autograding and student learning for the IU Intro to Computer Science course.
  • Graphite and Sawzall, which aim to make Racket a better language for data science, and make typesetting academic papers with data visualizations easier.
  • types.pl, a general-purpose Fediverse instance for people studying programming languages or related fields.

Because multiple people have emailed me and asked: I will not work on your blockchain, cryptocurrency, web3, NFT, et cetera project.

Contact

  • Email: hazel@knightsofthelambdacalcul.us (If you’re emailing me, use PGP or include the word “cactus” in your email.)
  • GitHub: @ralsei (Only used for collaborative projects. Otherwise, see the Git link above.)
  • Mastodon: @hazel@types.pl
  • Twitter: @sonicisdead (This is mostly a mirror of my Mastodon.)
  • DMs: email me and ask, but I would probably prefer the contact methods above.

Encryption

  • PGP: 5930 67D3 5E5C A280 959C EC37 35C1 2057 1662 1182
  • age: age1fjfm6qm9g5w7fr4vnf0uyu06aw5wdgaa67ln083u3dflleu7u59sek7whd
  • minisign/signify: RWQMcbd+Zp5RLkWLCJvnlElLOm9SEFEsgV1eU2IafmRnDPTrak/whUyD