Skip to main content
Proof Assistants Beta
András Kovács's user avatar
András Kovács's user avatar
András Kovács's user avatar
András Kovács
  • Member for 2 years, 5 months
  • Last seen this week
Profile Activity
Stats
2,077
reputation
8k
reached
18
answers
0
questions
Communities
View all
About

Type theory researcher at ELTE Budapest.

Badges
View all badges
This user doesn’t have any gold badges yet.
9
silver badges
17
bronze badges
Top tags
View all tags
66
Score
5
Posts
28
Posts %
64
Score
9
Posts
50
Posts %
49
Score
4
Posts
22
Posts %
45
Score
3
Posts
17
Posts %
39
Score
2
Posts
11
Posts %
33
Score
4
Posts
22
Posts %
Top posts
View all questions and answers
23
What are the complex induction patterns supported by Agda?
Feb 20, 2023
22
When should I use De Bruijn levels instead of indices?
Mar 1, 2022
17
Constructive proof of strong normalization for simply typed lambda calculus
Mar 23, 2022
16
Easy ways to introduce inductive types
Mar 8, 2022
11
What is hereditary substitution and why should I use it?
Mar 27, 2022
11
What are the upsides and downsides of typed vs untyped conversion?
Feb 20, 2022
10
Replacing (strict) positivity with monotonicity on propositions
Apr 4, 2022
9
Is it possible to define `fib` coinductive stream w/o sized types?
Feb 13, 2022
9
Strong eta-rules for functions on sum types
Dec 10, 2022
7
Normalization by evaluation for extensional type theories
May 13, 2022
Top network posts
View all network posts
104
Erratic hole type resolution
66
Haskell program involving `read` is much slower than an equivalent Python one
33
Doing rank-n quantification in Idris
31
Compatibility of impredicative Set and function extensionality
27
Online reference book for *implementing* concepts in type theory.