Korkut

Computer scientist.

I am a researcher at Bloomberg's CTO Infrastructure and Security Research team in New York City, applying formal methods in industry.

I'm also a PhD candidate in computer science at Princeton University's programming languages group, advised by Andrew W. Appel, working on VeriFFI, a foreign function interface between Coq and C, on the CertiCoq compiler, verified via VST. I plan to graduate in November 2024.

I'm interested in compilers, type systems, formal verification, metaprogramming, property-based testing, separation logic.

You can reach me at jkorkut@bloomberg.net regarding my work at Bloomberg or joomy@type.systems for other matters.

My CV is available here, as well as other online profiles: Twitter, Mastodon, Google Scholar, ORCID, LinkedIn, alphaXiv.

Internship

I am looking for interns for the summer of 2025, but other timelines are also possible. If you are interested, please reach out to me at my Bloomberg e-mail address.

Written Work

Foreign Function Verification Through Metaprogramming (draft). Joomy Korkut. PhD dissertation. Princeton University. 2024.
[PowerPoint slides] [Coq code]
A Verified Foreign Function Interface Between Coq and C. Joomy Korkut, Kathrin Stark, Andrew W. Appel. Submitted, 2024.
[Coq code]
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. Wesleyan University. 2018.
[Idris code for demos] [Idris code for Hezarfen] [Poster]
Thinking Outside the □: Verified Compilation of ML5 to JavaScript. Joomy Korkut. Undergraduate senior thesis. Wesleyan University. 2017.
[Agda code] [Poster]
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: