Assistant Professor at the University of Regina.
Formerly a Newton International Fellow at the University of Edinburgh with Ohad Kammar, and before that, PhD at UBC with Ron Garcia.
Broadly interested in making it easier to prove software correct with dependent types. Projects include dependent pattern matching, gradual dependent types, and error message generation.
|
2d
|
|
awarded | Electorate |
|
Jul
14 |
|
answered | Why does Agda use Set instead of Type? |
|
Jul
14 |
|
comment |
Why does Agda use Set instead of Type? I don't know enough of the history to answe on thst, but I always got the impression it's a historical thing to try to make it look more like conventional math, and the Type/Set distinction in HoTT came later |
|
Jul
11 |
|
answered | Languages and Turing Machine |
|
Jun
21 |
|
answered | Why did this proof succeed without function extensionality? |
|
Jun
20 |
|
awarded | Custodian |
|
Jun
20 |
|
reviewed | Approve suggested edit on Org-mode code blocks and results side-by-side in beamer export? |
|
Jun
19 |
|
asked | org-babel: Pass flags when filtering source code blocks? |
|
Jun
19 |
|
comment |
Org-mode code blocks and results side-by-side in beamer export? Perfect, this is just what I'm looking for! Is there any way to make a shorthand for this so I don't have to type out the PROPERTIES each time? |
|
Jun
19 |
|
accepted | Org-mode code blocks and results side-by-side in beamer export? |
|
Jun
18 |
|
awarded | Critic |
|
Jun
18 |
|
asked | Org-mode code blocks and results side-by-side in beamer export? |
|
Jun
18 |
|
accepted | Org-babel ignores RESULTS when generating beamer? |
|
Jun
18 |
|
comment |
Org-babel ignores RESULTS when generating beamer? @NickD Perfect, that did it. It there any way to set that for all code blocks as the default? |
|
Jun
18 |
|
comment |
Org-babel ignores RESULTS when generating beamer? @NickD what does that do? I tried it but it didn't seem to change anything, but maybe something else is interfering |
|
Jun
17 |
|
asked | Org-babel ignores RESULTS when generating beamer? |
|
Jun
7 |
|
awarded | Yearling |
|
Jun
7 |
|
awarded | Yearling |
|
Jun
7 |
|
comment |
Culture of conferences and registration fees @feynman Not saying that conferences don't have fees, but a conference that doesn't get you anything for those fees (e.g. no food) |
|
Jun
5 |
|
comment |
Culture of conferences and registration fees @feynman Are you sure the conference you're looking at isn't predatory? |