Stack Exchange

gallais

Glasgow, Scotland

http://www.gallais.org

top accounts reputation activity favorites subscriptions
Top Questions
Top Answers
21
How do I verify the Coq proof of Feit-Thompson?
mathoverflow.net

17
Open Type Level Proofs in Haskell/Idris
stackoverflow.com

15
How to switch the current goal in Coq?
stackoverflow.com

14
Why does Coq have Prop?
cstheory.stackexchange.com

13
Coq execution difference between semicolon “;” and period “.”
stackoverflow.com

13
Is it possible to use church encodings without breaking equational reasoning?
stackoverflow.com

11
List based on right Kan extension
stackoverflow.com

11
Proof assistant for mathematics only
stackoverflow.com

11
How can I rewrite “+ 1” (plus one) to “S” (succ) in Coq?
stackoverflow.com

11
“Minimal” intuitionistic type theory?
cs.stackexchange.com

11
Can a type system serve as a proof assistant for foreign functions?
cs.stackexchange.com

10
Type theory and computational complexity
cstheory.stackexchange.com

10
How to map Type to Value in Idris/Agda/Coq?
stackoverflow.com

10
Could not deduce KnownNat in two existentials with respect to the singletons library
stackoverflow.com

9
What does an apostrophe in front of a list ( '[Something] ) mean in Haskell?
stackoverflow.com

9
Is it possible to evaluate lambda calculus terms efficiently?
stackoverflow.com

8
What is the correct definition of `unfold` for an untagged tree?
stackoverflow.com

8
How do I refer to the same type variable in different type annotations?
stackoverflow.com

8
Idris non-trivial type computation for tensor indexing
stackoverflow.com

8
What should I do if two modules share the same name?
stackoverflow.com

7
Haskell: How is Num held?
stackoverflow.com

7
Why are ML/Haskell datatypes useful for defining “languages” like arithmetic expressions?
stackoverflow.com

7
Type Level Fix Point while Ensuring Termination
stackoverflow.com

7
Proving a sorting operation in type system
cs.stackexchange.com

7
Coq proof that type isomorphism relationship is transitive
codereview.stackexchange.com

7
Casting a nullary data constructor between types
softwareengineering.stackexchange.com

7
Is there a way to emulate linear types in Haskell?
stackoverflow.com

7
How to define abstract types in agda
stackoverflow.com

7
How to disable my custom notation in Coq?
stackoverflow.com

7
Might laziness also mean a value of function depends on context where it is called?
stackoverflow.com

1 2 3