Block or report user

Organizations

@barnowl @mitex @sipb @mit-plv

Pinned repositories

  1. HoTT/HoTT

    Homotopy type theory

    Coq 582 114

  2. lob

    Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/)

    Coq 11

  3. coq-tools

    Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

    Python 13 2

  4. social-interactions

    Musings on social interactions and emotions

    5 1

  5. coq-scripts

    Various useful scripts for dealing with Coq files

    Coq 1 1

  6. lob-paper

    A write-up of https://github.com/JasonGross/lob

    Agda 1 1

1,943 contributions in the last year

Jul Aug Sep Oct Nov Dec Jan Feb Mar Apr May Jun Mon Wed Fri

Contribution activity

June 2018

Created a pull request in mit-plv/fiat-crypto that received 2 comments

[WIP] Experiments no cps with rewrites extraction to string

Mostly for visibility. This is the full pipeline, with the rewriter, without cps, with to-C-stringification, with extraction

+409,916 −5,599 2 comments

Created an issue in coq/coq that received 8 comments

Extraction runs out of memory after eating 60 GB of RAM

Version 8.8.0 Description of the problem slow-extraction.tar.gz Run make. The relevant files for extraction are in src/Experiments/NewPipeline/Extr…

8 comments

Seeing something unexpected? Take a look at the GitHub profile guide.