Loïc

Member for 1 year, 10 months
Last seen more than a week ago

Summary

Reputation

1,409

1.4k
1.4k
1.3k

Mar
Jun
Sep
Dec

Top tag

dependent-type

Next privilege

1,500 Rep.

Approve tag wiki edits

Badges

9

15

Newest

Nice Answer

Next badge

0/1

Excavator

Answers

View all 6 answers

Score Activity Newest

40

Has anyone ever accidentally "proven" a false theorem with type-in-type?

Mar 31, 2022

26

Proof-theoretic comparison table?

Mar 30, 2022

25

Is there a way to automatically translate proofs from one proof assistant to another?

Feb 9, 2022

13

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

Feb 9, 2022

11

What are the possible kinds of type theories or logics with quotients?

Feb 14, 2022

Questions

Score Activity Newest Views

This user has not asked any questions

Tags

View all 15 tags

dependent-type

40

Score

1

post

calculus-of-inductive-constructions

36

Score

2

posts

foundations

26

Score

1

post

set-theory

26

Score

1

post

predicativity

26

Score

1

post

Reputation

+30

Proof-theoretic comparison table?

+10

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

+10

Has anyone ever accidentally "proven" a false theorem with type-in-type?

+10

What is Artin gluing, and how is it useful in proving meta-theoretic properties?

Badges

View all badges

This user doesn’t have any gold badges yet.

9

silver badges

Guru

Oct 5
Good Answer

× 3

Nov 10
Beta

Mar 15, 2022

15

bronze badges

Announcer

Jun 6, 2022
Commentator

Feb 11, 2022
Caucus

Mar 30, 2022

Accounts

Proof Assistants

1,409
9
15

101
2

Theoretical Computer Science

101
2

Active bounties (0)

Active Offered Earned

This user has no active bounties

Votes cast

86

upvotes

4

downvotes

36

question votes

54

answer votes