Theoretical Computer Science
gallais
  • gallais.org
  • Glasgow, Scotland, UK
  • Member for 10 years, 5 months
Profile Activity
Stats
626
reputation
9k
reached
9
answers
0
questions
Communities
View all
Badges
View all badges
This user doesn’t have any gold badges yet.
4
silver badges
14
bronze badges
Top tags
View all 15 tags
23
Score
4
Posts
44
Posts %
23
Score
4
Posts
44
Posts %
16
Score
3
Posts
33
Posts %
16
Score
2
Posts
22
Posts %
11
Score
2
Posts
22
Posts %
10
Score
1
Posts
11
Posts %
Top posts
All Questions Answers
Votes Newest
14
Why does Coq have Prop?
Mar 31 '14
10
Type theory and computational complexity
Oct 25 '18
6
Typing of substitution in a bidirectional type system
Nov 2 '18
5
Translation from basic While-language to $\lambda$-calculus
May 19 '11
5
What are the negative consequences of extending CIC with axioms?
Dec 19 '15
2
A formal grammar for P?
May 20 '11
2
Is there an algorithm to generate proof in Coq?
Jul 31 '15
2
Formalization of dependent record types/kinds in MLTT or variant thereof?
Sep 3 '19
2
Non-termination, strict positivity and free monads
Feb 27 '20
Top network posts
View all
24
How do I verify the Coq proof of Feit-Thompson?
20
How to switch the current goal in Coq?
17
Open Type Level Proofs in Haskell/Idris
16
Coq execution difference between semicolon ";" and period "."
13
Is it possible to use church encodings without breaking equational reasoning?

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.