Pinned Repositories
amazeui
Amaze UI, a mobile-first and modular front-end framework.
arm-trusted-firmware
Read-only mirror of Trusted Firmware-A
armv8a-address-translation
ARMv8-A Address Translation: Isabelle Proof Scripts
audiosprite
Howler.js compatible audio sprite generator
c0-compiler
c0 compiler with lex and yacc in C
c0compiler
编译原理上机作业--C0编译器
capflow
Isabelle proof for CapFlow
Carson
concrete-semantics
My solutions to exercises in "Concrete Semantics" (Tobias Nipkow, Gerwin Klein)
concrete-semantics-book
Self study log of the book
applepingge's Repositories
applepingge/arm-trusted-firmware
Read-only mirror of Trusted Firmware-A
applepingge/c0compiler
编译原理上机作业--C0编译器
applepingge/embedded-iot_profile
embedded-iot_profile
applepingge/google-access-helper
谷歌访问助手破解版
applepingge/grammars-v4
Grammars written for ANTLR v4; expectation that the grammars are free of actions.
applepingge/HOL
Canonical sources for HOL4 theorem-proving system. Branch `develop` is where “mainline development” occurs; when `develop` passes our regression tests, `master` is merged forward to catch up.
applepingge/L4Thread
applepingge/L4ThreadManagement
applepingge/lem
Lem semantic definition language
applepingge/linux
Linux kernel source tree
applepingge/linux-insides
A little bit about a linux kernel
applepingge/llvm-project
The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at http://reviews.llvm.org.
applepingge/NARUTO
applepingge/opam
opam is a source-based package manager. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.
applepingge/optee_os
Trusted side of the TEE
applepingge/pistachio
L4Ka::Pistachio micro-kernel
applepingge/practical-fm
A gently curated list of companies using verification formal methods in industry
applepingge/racket-book
My racket study documentation
applepingge/sail-arm
Sail version of ARM ISA definition, currently for ARMv8.5-A
applepingge/seL4
The seL4 microkernel
applepingge/serval
applepingge/serval-sosp19
This repo contains the artifact for our SOSP'19 paper on Serval
applepingge/serval-tutorial-sosp19
applepingge/Storybook
applepingge/test
applepingge/tlb
Formal Isabelle/HOL model of the ARMv7 TLB
applepingge/Tscheme
a experiment to implement HM type system on Racket/scheme
applepingge/utp-main
An implementation of Hoare and He's Unifying Theories of Programming in Isabelle
applepingge/viap_updated
applepingge/z3
The Z3 Theorem Prover