User Portlet

I'm a student interested in many aspects of various technical disciplines. Most of my interest lies in the foundations of computer science and mathematics.

I have a good knowledge base on formal logic, axiomatic set theory, type theory, and category theory. I'm currently researching the relation between category theory and type theory (categorical logic) and applications of higher category theory to type theory, specifically a topic called Directed HoTT.

I also know a bit about physics, up to Hamiltonian mechanics and some quantum mechanics. One of the things I do periodically is write up simulations of various physical systems. Recently, a very efficient gravity/electric simulator and a quantum computer "emulator", of sorts.

I also have a lot of programming experience, and have made projects in many languages, including C, C++, Python, JavaScript, Haskell, and of course The Wolfram Language. I've dabbled in many others, but those are the ones I feel confident writing my projects in.

I'm currently expanding my experience with dependently typed programming langues, recently NuPRL, Andromeda, and CubicalTT.. I'm hoping to one day make my own language (or be part of such a project) that combines aspects of logic programming and dependent types, a-la Curry. I do have some hobby experience writing interpreters and target-compilers.

I don't tend to stick to one project long enough to have much to show for my efforts. I usually start something, get it working, then archive it.