hiroki-chen
CS Ph.D. @ IUB "Algorithms are the computational content of proofs." (Robert Harper)
UnemployedSaratoga, CA
Pinned Repositories
incubator-teaclave-sgx-sdk
Apache Teaclave (incubating) SGX SDK helps developers to write Intel SGX applications in the Rust programming language, and also known as Rust SGX SDK.
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
FH_cryptDB
This is an advanced FH-CryptDB based on CryptDB prototype written by Popa et al.
lambda-rs
A dependently typed lambda calculus interpreter
NeoOS
A tiny operating system built with Rust.
NKUCompiler
kani
Kani Rust Verifier
nvtrust
Ancillary open source software to support confidential computing on NVIDIA GPUs
occlum
Occlum is a memory-safe, multi-process library OS for Intel SGX
prusti-dev
A static verifier for Rust, based on the Viper verification infrastructure.
hiroki-chen's Repositories
hiroki-chen/NeoOS
A tiny operating system built with Rust.
hiroki-chen/lambda-rs
A dependently typed lambda calculus interpreter
hiroki-chen/SGXOram
SO2 ORAM implementation and evaluation
hiroki-chen/SSE-SEAL
Searchable Encryption with Adjustable Leakage
hiroki-chen/Coq-Resources
A collection of useful tools, materials, tricks for Coq
hiroki-chen/hiroki-chen.github.io
Github Pages template for academic personal websites, forked from mmistakes/minimal-mistakes
hiroki-chen/nvtrust-rs
A Rust-based CLI tool for configuring the Nvidia's Hopper H100 CC on host
hiroki-chen/AMDSEV-kernel
AMD Secure Encrypted Virtualization
hiroki-chen/coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
hiroki-chen/Coq-RDB
A backup of Harvard's YNOT project which is lost
hiroki-chen/differential-privacy
Google's differential privacy libraries.
hiroki-chen/differential-privacy-rs
Rust bindings to Google's Differential Privacy Library.
hiroki-chen/duckdb
DuckDB is an in-process SQL OLAP Database Management System
hiroki-chen/duckdb-rs
Ergonomic bindings to duckdb for Rust
hiroki-chen/hiroki-chen
hiroki-chen/incubator-teaclave
Apache Teaclave (incubating) is an open source universal secure computing platform, making computation on privacy-sensitive data safe and simple.
hiroki-chen/Lean-Playground
Learning the Lean4 proof assistant and type theory!
hiroki-chen/MIRAI
Rust mid-level IR Abstract Interpreter
hiroki-chen/nvtrust
Ancillary open source software to support confidential computing on NVIDIA GPUs
hiroki-chen/opendp
The core library of differential privacy algorithms powering the OpenDP Project.
hiroki-chen/polars
Dataframes powered by a multithreaded, vectorized query engine, written in Rust
hiroki-chen/principles-of-programming-language
hiroki-chen/risc0
RISC Zero is a zero-knowledge verifiable general computing platform based on zk-STARKs and the RISC-V microarchitecture.
hiroki-chen/Software-Foundations
Exercises for the course.
hiroki-chen/spark
Apache Spark - A unified analytics engine for large-scale data processing
hiroki-chen/sqlite
Official Git mirror of the SQLite source tree
hiroki-chen/statrs
Statistical computation library for Rust
hiroki-chen/syzkaller
syzkaller is an unsupervised coverage-guided kernel fuzzer
hiroki-chen/tdx-tools
hiroki-chen/TPC-H-benchmark