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 1 year, 10 months
  • Last seen more than a week ago
Profile Activity
Stats
2,007
reputation
7k
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.
8
silver badges
16
bronze badges
Top tags
View all tags
63
Score
9
Posts
50
Posts %
63
Score
5
Posts
28
Posts %
47
Score
4
Posts
22
Posts %
42
Score
3
Posts
17
Posts %
39
Score
2
Posts
11
Posts %
31
Score
2
Posts
11
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
answer
22
When should I use De Bruijn levels instead of indices?
Mar 1, 2022
answer
21
What are the complex induction patterns supported by Agda?
Feb 20
answer
17
Constructive proof of strong normalization for simply typed lambda calculus
Mar 23, 2022
answer
13
Easy ways to introduce inductive types
Mar 8, 2022
answer
11
What are the upsides and downsides of typed vs untyped conversion?
Feb 20, 2022
answer
10
What is hereditary substitution and why should I use it?
Mar 27, 2022
answer
10
Replacing (strict) positivity with monotonicity on propositions
Apr 4, 2022
answer
9
Strong eta-rules for functions on sum types
Dec 10, 2022
answer
8
Is it possible to define `fib` coinductive stream w/o sized types?
Feb 13, 2022
answer
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.

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.