Skip to main content
Theoretical Computer Science
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel's user avatar
Dan Doel
  • Member for 13 years, 11 months
  • Last seen this week
  • Boston, MA, USA
Profile Activity

17 Answers

Score Activity Newest
11 votes
Accepted

How do continuations represent negations (under the Curry–Howard correspondence)?

11 votes
Accepted

Stronger "induction" principles than induction-recursion

10 votes
Accepted

Is Church-pentation implementable in Agda?

8 votes

What happens when the Linz halting problem proof is based on simulation of the input?

7 votes

Reader, Writer monads

4 votes
Accepted

Is there a relation between the techniques used by Dan Willard, versus those of Brown and Palsberg, to exclude diagonalization?

4 votes
Accepted

Is Linear Evaluation Parametric?

4 votes
Accepted

Is the Mendler-encoding in System-F adequate?

3 votes
Accepted

Can you always throw away the types when evaluating lambda expressions?

3 votes

Why/when do we ever need transfinite loop variants?

3 votes

Can Non-termination be considered an algebraic effect?

3 votes
Accepted

How to encode a function from an existential type

2 votes

Do realizable systems always have some non-well-founded sets?

1 vote
Accepted

Formalising Church numerals in Agda

1 vote

What category are Tagless Final Algebras final In?

1 vote
Accepted

Intuition behind nested positivity and counterexamples

1 vote

Under what models do we know linear time sorting?