Korkut

PhD student in computer science at Princeton University.

I'm a fifth year grad student, advised by Andrew W. Appel, working on VeriFFI, a foreign function interface between Coq and C, on the CertiCoq compiler, verified via VST.

I'm a member of the programming languages group; I'm interested in dependent types, formal verification, proof automation, metaprogramming, and computational linguistics.

Before starting a PhD program, I was at Wesleyan University (BA, MA), working with Daniel R. Licata on compiler verification and editor interaction for dependently typed languages.

You can reach me at joomy@cs.princeton.edu, or look at my CV, blog, or my Twitter and Mastodon posts.

On the job market

I am looking for industry positions, especially as a software engineer, a compiler engineer, or an applied scientist.
Feel free to reach me if you are hiring for such a position.
You can find my CV here. My expected graduation date is October 2023.

Teaching

I am not teaching right now.
However, if you need to see me, you can e-mail me to set up a meeting on Zoom or Skype.

Papers

A Proof Tree Builder for Sequent Calculus and Hoare Logic. Joomy Korkut. ThEdu '22, published in EPTCS. 2022.
[Video] [Application link] [JavaScript code]
Morphology and Lexicon-based Machine Translation of Ottoman Turkish to Modern Turkish. Joomy Korkut. Unpublished draft, 2019.
[Haskell code]
Extensible Type-Directed Editing. Joomy Korkut, David Thrane Christiansen. TyDe ’18, 2018.
Edit-Time Tactics in Idris. Joomy Korkut. Master's thesis. 2018.
[Idris code for demos] [Idris code for Hezarfen]
Thinking Outside the □: Verified Compilation of ML5 to JavaScript. Joomy Korkut. Undergraduate senior thesis. 2017.
[Agda code]
Intrinsic Verification of a Regular Expression Matcher. Joomy Korkut, Maksim Trifunovski, Daniel R. Licata. Unpublished draft. 2016.
[Agda code]

Talks

Ergonomics and verification of a foreign function interface between Coq and C, general exam talk, May 14th, 2020.
[PDF slides]
Direct Reflection for Free!, at ICFP 2019 Student Research Competition finalist talks (bronze medal), August 20th, 2019.
[PDF poster] [PDF slides] [Keynote slides] [Haskell code]
Commanding Emacs from Coq, at Scheme Workshop 2019, August 18th, 2019.
[Video] [PDF slides] [Coq and Emacs Lisp code]
Direct Reflection for Free!, at New York Seminar on Programming Languages and Software Engineering, February 25th, 2019.

Last updated: