Skip to content
View markusdemedeiros's full-sized avatar

Block or report markusdemedeiros

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
markusdemedeiros/README.md

I'm Markus (he/him).

My website is markusde.ca.

I like writing proofs. I like writing programs that look like proofs.

Pinned Loading

  1. Eileen Eileen Public

    Reimplementing some data structures from Iris in Lean

    Lean 2

  2. Order Order Public

    Lean Formalization of "Bringing Order to the Separation Logic Jungle"

    Lean

  3. whynot86 whynot86 Public

    A collection of tiny Y86 programs for fun and profit

    Assembly

  4. ATheoryOfPrograms ATheoryOfPrograms Public

    Typesetting of Dana Scott and J.W. de Bakker's unpublished notes at IBM Vienna 1969

    TeX 8

  5. logsem/clutch logsem/clutch Public

    Probabilistic separation logics for verifying higher-order probabilistic programs.

    Coq 20 4

  6. leanprover/SampCert leanprover/SampCert Public

    SampCert : Verified Differential Privacy

    Lean 69 7