András Kovács
where else to find them
no profile links on file
what they talk about
where they keep going back
on a stage with
never shared a talk
who talks about the same things
- Kristina Sojakova3 talks
- Andrei Popescu5 talks
- Andreas Abel6 talks
- Alexander Konovalov8 talks
- Stephan Boyer4 talks
- Ambrus Kaposi2 talks
| title | conference | date |
|---|---|---|
| Observing Definitional Equality | WITS 2026 | 2026-01-17 |
Proposes replacing the usual dependent observational equality used in heterogeneous unification (Gundry, McBride, Juan) with homogeneous observational equality… | ||
| Canonicity for Indexed Inductive-Recursive Types | POPL 2026 | 2026-01-11 |
Proves canonicity for Martin-Löf type theory with a countable universe hierarchy where every universe supports indexed inductive-recursive types. Method is two… | ||
| Eta conversion for the unit type (is still not that simple) | WITS 2025 | 2025-01-25 |
Argues that eta for unit needs type-directed conversion and proposes a bidirectional elaboration core interleaved with normalization-by-evaluation that… | ||
| Efficient Evaluation with Controlled Definition Unfolding | WITS 2024 | 2024-01-20 |
Proposes an evaluator-for-elaboration that preserves definition unfoldings by representing top-level names as delayed top-level unfolding nodes in the semantic… | ||
| Staged Compilation with Two-Level Type Theory | ICFP 2022 | 2022-09-11 |
Shows that two-level type theory (2LTT) can serve as a foundation for staged compilation that supports full dependent types, provides a staging-by-evaluation… | ||
| Elaboration with First-Class Implicit Function Types | ICFP 2020 | 2020-08-23 |
Presents an elaboration algorithm that actually inserts implicit lambdas by extending core Martin-Löf type theory with strictly curried function types and… | ||
| nothing matches | ||