Skip to main content
Proof Assistants Beta
Meven Lennon-Bertrand's user avatar
Meven Lennon-Bertrand's user avatar
Meven Lennon-Bertrand's user avatar
Meven Lennon-Bertrand
Moderator
  • Member for 2 years, 5 months
  • Last seen more than a week ago
Profile Activity
Stats
5,530
reputation
32k
reached
109
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
28
bronze badges
Top tags
View all tags
184
Score
62
Posts
55
Posts %
46
Score
10
Posts
9
Posts %
37
Score
8
Posts
7
Posts %
31
Score
9
Posts
8
Posts %
29
Score
8
Posts
7
Posts %
28
Score
10
Posts
9
Posts %
Top posts
View all questions and answers
26
What are the differences between MLTT and CIC?
Feb 10, 2022
19
Does the canonicity of natural number imply that of all types?
Mar 11, 2022
18
What are the complex induction patterns supported by Agda?
Feb 9, 2023
13
In what intensional type theories can absurdity be made definitionally proof irrelevant?
Feb 24, 2022
12
Why are impredicative constructions used less in type theory than in material set theory?
Sep 23, 2022
11
Explanation of Coq math-comp repositories
Apr 15, 2022
10
Is internal parametricity useful in theorem proving?
Feb 9, 2022
10
Is eta-equality provable in Coq?
Feb 10, 2022
9
What is the trade-off to accepting impredicative propositions?
Mar 7, 2022
9
How can we formalize a game where each player is a program having access to opponent's code?
Oct 11, 2022
Top network posts
View all network posts
6
Double-headed squiggly arrow
5
Software Foundations Volume 1: Tactics: injection_ex3