Skip to main content
Proof Assistants Beta
Jason Gross's user avatar
Jason Gross's user avatar
Jason Gross's user avatar
Jason Gross
  • Member for 2 years, 7 months
  • Last seen this week
Profile Activity
Stats
1,547
reputation
5k
reached
18
answers
2
questions
Communities
View all
About

I began a PhD program at MIT in computer science (specifically programming languages) in the fall of 2013. I majored in mathematics and physics as an undergrad at MIT. I'm especially interested in category theory, homotopy type theory, interactive proof assistants, general relativity, quantum mechanics, topology, and education. I've been working on developing a category theory library in Coq with David Spivak and Adam Chlipala, with an eye towards applications to databases.

Badges
View all badges
This user doesn’t have any gold badges yet.
4
silver badges
11
bronze badges
Top tags
View all tags
29
Score
2
Posts
10
Posts %
27
Score
1
Posts
5
Posts %
27
Score
1
Posts
5
Posts %
27
Score
1
Posts
5
Posts %
25
Score
8
Posts
40
Posts %
20
Score
3
Posts
15
Posts %
Top posts
View all questions and answers
answer
27
What are the bases for different Proof Assistants?
Feb 8, 2022
question
20
What is known about performance bottlenecks in proof assistants?
Feb 15, 2022
answer
10
Are there automated theorem provers for constructive logics? What strategy do they use?
Feb 13, 2022
answer
8
Have any proof assistants incorporated a notion of unsafety with Type : Type?
Feb 13, 2022
answer
7
Are there any proof assistants which integrate JITs?
Feb 9, 2022
answer
7
Why do record based inductive types with primitive projections lack an eta law?
Jun 10, 2022
answer
7
Mechanization of game semantics?
Jun 10, 2022
answer
7
Counterexamples in Type Theory
Dec 28, 2022
answer
5
Is there a Proof assistant that is an esoteric programming language?
Feb 9, 2022
answer
5
Proof Review: Basic theorem about ternary relations in Coq
Feb 17, 2022
Top network posts
View all network posts
42
Formalizations of category theory in proof assistants
25
std::cout equivalent at compile time, or static_assert stringification of compile-time constant values in c++11
21
How do we construct the Gödel’s sentence in Martin-Löf type theory?
20
How do I make an attached file display like a link?
18
Formalizations of category theory in proof assistants