Korkut

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

I finished my PhD in computer science at Princeton University, advised by Andrew W. Appel, in 2024.*

I am interested in functional programming languages, compilers, type systems, and formal verification (especially with interactive theorem provers, such as Coq and Agda). I am particularly interested in applications of metaprogramming, property-based testing, and 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, GitHub, alphaXiv, Stack Overflow, Last.fm, Spotify.

In my free time, I play the fretless bass, occasionally translate literature, and sing a bit.

Academic Work

Foreign Function Verification Through Metaprogramming. Joomy Korkut. PhD dissertation. Princeton University. 2024.
[Coq code] [PowerPoint slides] [PDF slides] [PDF slides with speaker notes]
A Verified Foreign Function Interface Between Coq and C. Joomy Korkut, Kathrin Stark, Andrew W. Appel. (conditionally accepted to POPL 2025). 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]

Selected Talks

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]

English / Türkçe

Recent blog posts

Son blog yazıları

Intrinsic vs. extrinsic verification. October 30, 2024.
Tracing the origin of the terms "intrinsic" and "extrinsic" in formal verification and programming languages.
After ICFP 2018. September 30, 2018.
I spent a week at the main functional programming conference and got to talk to my heroes, so here are some reflections.
The diacritic omission phenomenon. November 18, 2017.
Omitting the diacritics is a common phenomenon in languages such as Turkish and Serbo-Croatian. Then why isn't there any research on this?

[RSS feed] [all posts]

Tags: conference (1), haskell (5), history (1), idris (2), language (2), logic (1), meta (1), pl (1), poetry (1), programming (1), prolog (1), proof assistants (1), proposal (1), teaching (1), translation (1), turkish (2), tutorial (1), wesleyan (1)

İlk yazı. October 28, 2024.
Bir giriş yazısı.

[RSS dağıtımı] [tüm yazılar]

Etiketler: blog (1)

Last updated: