Academic Work
-
Morphosyntactic Programming: Case, Mood, and Type-Directed Disambiguation for Turkish-Like Syntax. Joomy Korkut, Alperen Keles, Onur Akdemir. Draft in submission. 2026.
[Kip's source code] [Mechanized metatheory] -
Crane Lowers Rocq Safely into C++ (Extended Abstract). Matthew Z. Weaver, Joomy Korkut. RocqPL 2026. 2025.
[Video] [Rocq plugin code] -
A Rose Tree is Blooming (Proof Pearl). Joomy Korkut. CPP 2026. 2025.
[Video] [Rocq code] [PDF slides] [PDF slides with speaker notes] -
A Verified Foreign Function Interface between Coq and C. Joomy Korkut, Kathrin Stark, Andrew W. Appel. POPL 2025. 2024.
[Rocq code] [PowerPoint slides] [PDF slides] [PDF slides with speaker notes] [Video] -
Foreign Function Verification Through Metaprogramming. Joomy Korkut. PhD dissertation. Princeton University. 2024.
[DataSpace link] [LaTeX source] [Rocq code] [PowerPoint slides] [PDF slides] [PDF slides with speaker notes] -
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
-
From Proof to Practice: Extracting Verified Programs to Modern C++, keynote at LangSec Workshop at IEEE Security & Privacy, May 21st, 2026.
[PDF slides] [PDF slides with speaker notes] -
Direct Reflection for Free!, at ICFP 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, August 18th, 2019.
[Video] [PDF slides] [Rocq and Emacs Lisp code]
English / Türkçe
Recent blog posts
Son blog yazıları
-
Why I refuse to learn type-level programming in Haskell. November 23, 2025.
A short essay about why I refuse to learn complex language features like type-level programming in Haskell and first-class modules in OCaml. -
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.
-
Yakup Kadri'nin Ankara'sı üzerine düşünceler. November 11, 2024.
Ankara romanını okurken aklımdan geçenler üzerine bir şeyler yazmak istedim. -
İlk yazı. October 28, 2024.
Bir giriş yazısı.
Last updated: