Stack Exchange

cody

Cambridge, MA

http://www.andrew.cmu.edu/~croux/

I am currently an engineer at Draper Labs in Cambridge. My interests include software verification and language design, logic and computability, proof theory and other things.

top accounts reputation activity favorites subscriptions
Top Questions
Top Answers
45
What functions can System F not compute?
cstheory.stackexchange.com

36
Formal program verification in practice
cs.stackexchange.com

36
What makes type inference for dependent types undecidable?
cs.stackexchange.com

33
How to find interesting research problems
cstheory.stackexchange.com

30
Is Category Theory useful for learning functional programming?
cs.stackexchange.com

29
if (λ x . x x) has a type, then is the type system inconsistent?
cs.stackexchange.com

27
Algebra oriented branch of theoretical computer science
cstheory.stackexchange.com

24
What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?
cstheory.stackexchange.com

23
To what extent can an algorithm predict the time complexity an arbitrary input program?
cstheory.stackexchange.com

22
How do you get the Calculus of Constructions from the other points in the Lambda Cube?
cstheory.stackexchange.com

21
Is there a typed lambda calculus which is consistent and Turing complete?
cstheory.stackexchange.com

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

16
Relative consistency of PA and some type theories
cstheory.stackexchange.com

15
Is MLTT effectively pCiC without Prop?
cstheory.stackexchange.com

15
Are there any annotated formal verification systems for pure functional programming languages?
cstheory.stackexchange.com

15
Author ordering in TCS papers
cstheory.stackexchange.com

15
$\lambda$-calculus with reflection
cs.stackexchange.com

14
How is Lambda Calculus a specific type of Term Writing system?
cstheory.stackexchange.com

14
Logical Reations for an Impredicative System in a Predicative MetaTheory
cstheory.stackexchange.com

13
Is there an expressiveness hierarchy for type systems?
cstheory.stackexchange.com

13
Fixed point, what does it mean in the world of computer science
cs.stackexchange.com

12
Has a proof checker bug ever invalidated a major proof?
cstheory.stackexchange.com

12
Relation between type-checking decidability, typability decidability and strong normalization
cs.stackexchange.com

12
No Naive Set Theoretic Models of Polymorphic Lambda Calculus?
cs.stackexchange.com

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

12
funsplit and polarity of Pi-types
cstheory.stackexchange.com

12
Typo in the calculus of constructions paper?
cstheory.stackexchange.com

12
Is there a good notion of non-termination and halting proofs in type theory?
cstheory.stackexchange.com

11
Uses of $\infty$-categories in TCS
cstheory.stackexchange.com

11
Ramification of An Impredicative Type Theory
cstheory.stackexchange.com

1 2 3 4 5 6