ahuoguo

ahuoguo's Stars

• yallop/effects-bibliography

  A collaborative bibliography of work related to the theory and practice of computational effects

  99563486

• sweirich/pi-forall

  A demo implementation of a simple dependently-typed language

  Language:Haskell58433590

• elikaski/ECC_Attacks

  Known attacks on Elliptic Curve Cryptography

  Language:Sage3647224

• MPLLang/mpl

  The MaPLe compiler: efficient and scalable parallel functional programming

  Language:Standard ML358247621

• links-lang/links

  Links: Linking Theory to Practice for the Web

  Language:OCaml3331959143

• teorth/equational_theories

  A project to map out the relations between different equational theories of Magmas.

  Language:C286424367

• jeanqasaur/dsl-syllabus-fall-2016

  The syllabus from 15-819, the PhD seminar I taught on domain-specific programming languages fall 2016.

  2135011

• Generative-Program-Analysis/GenSym

  A high-performance, parallel, compilation-based symbolic execution engine

  Language:Java126614

• forestdb/forestdb.org

  A repository for generative models

  Language:JavaScript11429724

• OPLSS/introduction-to-algebraic-effects-and-handlers

  Introduction to algebraic effects and handlers

  Language:TeX941104

• kenmcmil/ivy

  IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.

  Language:C++8776426

• SHoltzen/dice

  Exact inference for discrete probabilistic programs. (Research code, more documentation and ergonomics to come)

  Language:OCaml8263620

• slindley/effect-handlers

  Language:Haskell821909

• GillianPlatform/Gillian

  The Gillian Platform main repository

  Language:OCaml81811715

• IBM/FormalML

  Formalization of Machine Learning Theory with Applications to Program Synthesis

  Language:Coq7512117

• aws/aws-encryption-sdk-dafny

  AWS Encryption SDK for Dafny

  Language:Rust36922519

• namin/lms-verify

  generative programming & verification

  Language:C32505

• lexa-lang/lexa

  Language:OCaml29200

• webyrd/midoriKanren

  Relational interpeter combining miniKanren-in-miniKanren and Scheme-in-miniKanren

  Language:Scheme161

• formalsec/wasp

  WASP was superseded by: https://github.com/OCamlPro/owi

  Language:OCaml14541

• probcomp/ADEV.jl

  Experimental port of ADEV to Julia

  Language:Julia11501

• secure-foundations/vest

  High-assurance and performant Rust-based parsing and serialization of binary data formats verified in Verus

  Language:Rust7422

• conrad-watt/wasm-pl-isabelle

  Language:Isabelle5411

• GLaDOS-Michigan/eecs498-f24

  A repository with the assignments, demos and lab exercises for EECS498-003/CSE598-008 in Fall 2024

  Language:Dafny51

• JetBrains-Research/HumanEval-Dafny

  Translating humaneval into dafny

  Language:Dafny4391

• ericthewry/interpreters

  An Implementation of Many of the Definitional Interpreters from John C. Reynold's 1972 paper

  Language:Haskell3200

• matthias-brun/verus-find

  A tool to search for Verus functions and lemmas

  Language:Rust3

• wasmfx/waeio

  a prototype WebAssembly effect-based I/O framework

  Language:C3100

• tchajed/ivy-to-mypyvy

  Convert an Ivy liveness problem to a mypyvy input file

  Language:Rust2301

• codyjrivera/ids-artifact

  Artifact for "Predictable Verification using Intrinsic Definitions" in PLDI 2024

  Language:Boogie1100