Formal Methods Engineer at Bedrock Systems Inc. — Iris/Coq/λ calculus/Haskell/Agda
-
Bedrock Systems Inc.
- Berlin, Germany
- http://blaisorblade.github.io/
Block or Report
Block or report Blaisorblade
Report abuse
Contact GitHub support about this user’s behavior. Learn more about reporting abuse.
Report abusePinned
-
-
evalFromToAbsMachines Public
A Functional Correspondence between Evaluators and Abstract Machines
Haskell 8
-
hoas-with-names Public
Represent functions using higher-order abstract syntax (HOAS) *using macros to save names*
596 contributions in the last year
Less
More
Contribution activity
March 2023
Created 13 commits in 3 repositories
Created 1 repository
- Blaisorblade/coq-elpi OCaml
Created a pull request in LPCIC/coq-elpi that received 3 comments
Clarify difference between coq.reduction.{vm,native}.norm
I could be wrong but I guessed from the name and from the source code. Feel free to rephrase as appropriate. cc @jhaag
+8
−7
•
3
comments