HarrisonGrodin

PhD Student in PL @ CMU CSD

Carnegie Mellon UniversityPittsburgh, PA

Pinned Repositories

agda-modtt
ModTT in Agda
Language:Agda11 3 00
ATPL24
Notes for Advanced Topics in Foundations of Programming Languages (Spring 2024)
Language:TeX17 5 20
Completion.jl
Knuth-Bendix completion algorithm
Language:Julia4 1 10
radical-julia
Radical ideas for the Julia language.
Language:Standard ML26 8 21
Rewrite.jl
An efficient symbolic term rewriting engine
Language:Julia77 8 46
Simplify.jl
Algebraic simplification in Julia
Language:Julia84 8 366
SpecialSets.jl
Representations of commonly-used sets
Language:Julia8 2 51
agda-calf
A cost-aware logical framework, embedded in Agda.
Language:Agda57 6 52
setup-sml
Set up a Standard ML environment and add it to the PATH
Language:JavaScript2 2 01

HarrisonGrodin's Repositories

HarrisonGrodin/Simplify.jl
Algebraic simplification in Julia
Language:Julia84 8 366
HarrisonGrodin/Rewrite.jl
An efficient symbolic term rewriting engine
Language:Julia77 8 46
HarrisonGrodin/radical-julia
Radical ideas for the Julia language.
Language:Standard ML26 8 21
HarrisonGrodin/ATPL24
Notes for Advanced Topics in Foundations of Programming Languages (Spring 2024)
Language:TeX17 5 20
HarrisonGrodin/agda-modtt
ModTT in Agda
Language:Agda11 3 00
HarrisonGrodin/SpecialSets.jl
Representations of commonly-used sets
Language:Julia8 2 51
HarrisonGrodin/Completion.jl
Knuth-Bendix completion algorithm
Language:Julia4 1 10
HarrisonGrodin/computational-type-theory-2021
Computational Type Theory, Spring 2021.
Language:Agda2 2 00
HarrisonGrodin/intrinsic-typing
Intrinsically typed encodings of programming languages.
Language:Agda2 2 00
HarrisonGrodin/JuliaCon2018
Resources from Rewrite.jl presentations at JuliaCon 2018.
Language:Jupyter Notebook2 1 0
HarrisonGrodin/JuliaCon2020
JuliaCon 2020 poster
Language:TeX2 2 0
HarrisonGrodin/structure-editor
Structure editor for a basic typed functional programming language
Language:Elm2 2 0
HarrisonGrodin/1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Language:Agda1 0
HarrisonGrodin/agda-stdlib
The Agda standard library
Language:Agda1 0
HarrisonGrodin/git-auto-commit-action
Automatically Commit changed Files back to Github with Github Actions
Language:Shell1 0
HarrisonGrodin/gitignore
A collection of useful .gitignore templates
1 0
HarrisonGrodin/plfa.github.io
An introduction to programming language theory in Agda
Language:HTML1 0
HarrisonGrodin/smackage
Smackage Package Manager for Standard ML
Language:Standard ML1 0
HarrisonGrodin/tt02-verilog-demo
Verilog Collatz computer for TT02
Language:Python1 0
HarrisonGrodin/TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
Language:Agda1 0