Junyoung Jang
where else to find them
no profile links on file
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 5 in the filters
who talks about the same things
- Brigitte Pientka15 talks
- Jason Z. S. Hu6 talks
- Youngju Song6 talks
- Ende Jin2 talks
- Kenji Maillard11 talks
- Nicolas Tabareau14 talks
| title | conference | date |
|---|---|---|
| McTT: A Verified Kernel for a Proof Assistant | ICFP 2025 | 2025-10-12 |
A fully verified kernel for core Martin‑Löf type theory is implemented in Rocq, proving normalization, consistency and injectivity of constructors and proving… | ||
| McTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory | WITS 2025 | 2025-01-25 |
A correct-by-construction Coq implementation of Martin-Löf type theory produces an end-to-end proof checker, with formalized cumulative universe hierarchy and… | ||
| Moebius: Metaprogramming using Contextual Types | POPL 2022 | 2022-01-16 |
Moebius provides a formal metaprogramming core: a multi-level contextual modal lambda-calculus that generates System F–style polymorphic code, lets open code… | ||
| nothing matches | ||