Stack Exchange

gallais

Glasgow, Scotland

http://www.gallais.org

top accounts reputation activity favorites subscriptions

Top Questions

Application of type-level arguments of Kind other than Type

haskell type-kinds asked Oct 13 '17 at 10:13

stackoverflow.com

Implicit arguments in a computed type in Coq

types coq asked Nov 9 '17 at 11:02

stackoverflow.com

Checking that two values have the same head constructor

haskell asked May 12 '17 at 18:10

stackoverflow.com

ghc does not report non-exhaustive pattern matches when using the `no-code` flag

haskell pattern-matching typechecking asked Dec 25 '14 at 12:47

stackoverflow.com

Memoizing an effectful function

haskell memoization unsafe-perform-io asked Sep 11 '15 at 14:33

stackoverflow.com

Top Answers

How do I verify the Coq proof of Feit-Thompson?

mathoverflow.net

Open Type Level Proofs in Haskell/Idris

stackoverflow.com

How to switch the current goal in Coq?

stackoverflow.com

Why does Coq have Prop?

cstheory.stackexchange.com

Coq execution difference between semicolon “;” and period “.”

stackoverflow.com

Is it possible to use church encodings without breaking equational reasoning?

stackoverflow.com

List based on right Kan extension

stackoverflow.com

Proof assistant for mathematics only

stackoverflow.com

“Minimal” intuitionistic type theory?

cs.stackexchange.com

Can a type system serve as a proof assistant for foreign functions?

cs.stackexchange.com

Type theory and computational complexity

cstheory.stackexchange.com

How to map Type to Value in Idris/Agda/Coq?

stackoverflow.com

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

stackoverflow.com

Could not deduce KnownNat in two existentials with respect to the singletons library

stackoverflow.com

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

stackoverflow.com

Is it possible to evaluate lambda calculus terms efficiently?

stackoverflow.com

What is the correct definition of `unfold` for an untagged tree?

stackoverflow.com

How do I refer to the same type variable in different type annotations?

stackoverflow.com

Idris non-trivial type computation for tensor indexing

stackoverflow.com

Is there a way to emulate linear types in Haskell?

stackoverflow.com

How to define abstract types in agda

stackoverflow.com

How to disable my custom notation in Coq?

stackoverflow.com

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

stackoverflow.com

Coq: keeping information in a match statement

stackoverflow.com

Define an inductive dependent-type with constraints on the type-parameter

stackoverflow.com

Type Level Fix Point while Ensuring Termination

stackoverflow.com

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

stackoverflow.com

What should I do if two modules share the same name?

stackoverflow.com

Haskell: How is Num held?

stackoverflow.com

Proving a sorting operation in type system

cs.stackexchange.com