Proof Assistants Beta
Meven Lennon-Bertrand's user avatar
Meven Lennon-Bertrand's user avatar
Meven Lennon-Bertrand's user avatar
Meven Lennon-Bertrand
  • Member for 2 years, 2 months
  • Last seen this week
Profile Activity
Stats
4,868
reputation
27k
reached
93
answers
4
questions
Communities
View all
About

Post-doc in computer science, in the great world of proof assistants.

Badges
View all badges
This user doesn’t have any gold badges yet.
8
silver badges
27
bronze badges
Top tags
View all tags
145
Score
48
Posts
49
Posts %
44
Score
10
Posts
10
Posts %
31
Score
6
Posts
6
Posts %
29
Score
8
Posts
8
Posts %
26
Score
8
Posts
8
Posts %
18
Score
7
Posts
7
Posts %
Top posts
View all questions and answers
question
25
What are the differences between MLTT and CIC?
Feb 10, 2022
answer
19
Does the canonicity of natural number imply that of all types?
Mar 11, 2022
question
15
What are the complex induction patterns supported by Agda?
Feb 9, 2023
answer
13
In what intensional type theories can absurdity be made definitionally proof irrelevant?
Feb 24, 2022
answer
12
Why are impredicative constructions used less in type theory than in material set theory?
Sep 23, 2022
answer
11
Explanation of Coq math-comp repositories
Apr 15, 2022
answer
10
Is internal parametricity useful in theorem proving?
Feb 9, 2022
answer
10
Is eta-equality provable in Coq?
Feb 10, 2022
answer
9
How can we formalize a game where each player is a program having access to opponent's code?
Oct 11, 2022
answer
9
What happened to Conor McBride's universe polymorphism proposal?
Feb 9, 2022
Top network posts
View all network posts
6
Double-headed squiggly arrow
5
Software Foundations Volume 1: Tactics: injection_ex3