András Kovács

Type theory & applications. Also on Mastodon:

[András Kovács @andrasKovacs6]

@effectfully https://t.co/9l3uO51clm Not implying that it's good for practical impl, but there's nothing wrong with W as far as type theory goes.

[András Kovács @andrasKovacs6]

I'm at POPL starting from Tuesday.

[András Kovács @andrasKovacs6]

New paper conditionally accepted at POPL 2026: https://t.co/KrI7jgwXht

[András Kovács @andrasKovacs6]

The TyDe 2025 submission deadline has been extended to 22 June. Please consider submitting! The workshop is in Singapore but remote presentations are possible. More info: https://t.co/aAjF8oYbct

[András Kovács @andrasKovacs6]

This week there was a nice HoTT/UF workshop + EuroProofNet workshop, here's my slides: https://t.co/EWutfkdOQ5 In a nutshell, it's about a type theory where you can specify and use any number of two-level type theories over various object languages, at the same time.

[András Kovács @andrasKovacs6]

TyDe 2025 call for papers and extended abstracts: https://t.co/97YvxwoG2C Please consider submitting!

[András Kovács @andrasKovacs6]

@gergo_erdi We don't get all relevance info from elaboration btw, that's because elaboration works under bound vars, while conversion works under arbitrary instantiations of bound vars to values. E.g. while checking the body of "f : (A : U) -> ..." we know nothing about A's relevance.

[András Kovács @andrasKovacs6]

My slides for the WITS 25 workshop: https://t.co/oXr9RJFy41 Abstract: https://t.co/1ee4yXcrca

[András Kovács @andrasKovacs6]

@gergo_erdi Computing no types is cheaper than computing some types. If a source program doesn't depend on unit eta, the best we can do is to compute no types. The question is, how often do people depend on unit eta. If rarely, the lazy relevance checking is better, if often, it's worse.

[András Kovács @andrasKovacs6]

Dependent types + runtime code generation: https://t.co/qtPNd9Kcax

[András Kovács @andrasKovacs6]

@kmett @scheminglunatic I wouldn't say that; tbh it's on my TODO list to look into staging + substructural object languages but right now I don't know much about it. I worked recently a bit on regions + staging, which looks quite promising already without substructural types. https://t.co/GpnLqA2LBQ

[András Kovács @andrasKovacs6]

@kmett @brazilian_bbg Yet another example of staging being better than begging the compiler.

[András Kovács @andrasKovacs6]

@Iceland_jack Lots of big changes would be needed. Stage-indexing in kinds, proper dependent types and non-erased generated types in code intended for compile time, polarized types in code intended for runtime. And ofc the RTS has a different structure than what I described.

[András Kovács @andrasKovacs6]

I wrote about a design for region memory management: https://t.co/GpnLqA2LBQ
I'm pretty excited about it. Hopefully I'll be able to actually implement it not too far in the future.

[András Kovács @andrasKovacs6]

A small note on specifying correctness of elaboration for type theories: https://t.co/PTY2FfYSsH

[András Kovács @andrasKovacs6]

@yforster_cs That one doesn't validate eta for functions.

[András Kovács @andrasKovacs6]

Pierre-Marie Pédrot recently explained to me a nice and simple proof that function extensionality is not provable in MLTT. I wrote some Agda and explanations for it here: https://t.co/gkCA0ti6Z1

[András Kovács @andrasKovacs6]

I have a new paper to appear at ICFP 2024: https://t.co/KTeRGwosfz

[András Kovács @andrasKovacs6]

I wrote about garbage collection: https://t.co/Vyt0z48gK5

[András Kovács @andrasKovacs6]

@ltchen_tw Well, many people including myself don't bother...