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 bookmarks subscriptions
Top Questions
Top Answers
48
What functions can System F not compute?
cstheory.stackexchange.com

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

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

37
Formal program verification in practice
cs.stackexchange.com

31
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

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

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

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

16
Author ordering in TCS papers
cstheory.stackexchange.com

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

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

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

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

14
Implementation of alpha equivalence
cstheory.stackexchange.com

13
Is compiler for dependent type much harder than an intepreter?
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
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

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

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

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

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

1 2 3 4 5 6