Skip to main content
TeX - LaTeX
Jason Gross's user avatar
Jason Gross's user avatar
Jason Gross's user avatar
Jason Gross
  • Member for 13 years, 8 months
  • Last seen this week
Profile Activity
Stats
2,169
reputation
42k
reached
8
answers
45
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.
16
silver badges
28
bronze badges
Top tags
View all tags
6
Score
7
Posts
13
Posts %
5
Score
7
Posts
13
Posts %
4
Score
4
Posts
8
Posts %
2
Score
5
Posts
9
Posts %
2
Score
4
Posts
8
Posts %
2
Score
4
Posts
8
Posts %
Top posts
View all questions and answers
20
How do I make an attached file display like a link?
May 10, 2011
17
Dividing dimensions to get a count
Dec 6, 2012
16
Removing brackets from biblatex references for lncs
Apr 15, 2014
13
Making register declarations local, Undefining a register (count, toks, etc.)
Dec 15, 2010
12
Why does \jobname give asterisks/stars instead of spaces, and how do I fix this?
Apr 4, 2011
10
Detecting \global, \long, \outer, \protected
Apr 12, 2011
9
How do I forbid pagebreaks inside urls without forbidding linebreaks?
Jan 11, 2021
8
Conditioning footnotes on where the \footnotemark is in the page
Nov 27, 2010
8
What's a reliable way to detect math mode (including align*)?
Oct 5, 2020
7
How do I make an attached non-pdf file display like a link?
Feb 28, 2015
Top network posts
View all network posts
42
Formalizations of category theory in proof assistants
27
What are the bases for different 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
What is known about performance bottlenecks in proof assistants?