Software Foundations Laboratory

Seoul, Korea

Pinned Repositories

clang-freeze
Language:C++3 18 01
CompCertM
Language:Coq6 11 45
CompCertR
Language:Coq4 9 14
crellvm
Crellvm: Verified Credible Compilation for LLVM
Language:Coq15 8 21
crellvm-llvm
LLVM for Crellvm: Verified Credible Compilation for LLVM
Language:C++6 7 00
llvm-freeze
Language:LLVM5 19 131
llvmtwin-coq
Coq formalization of LLVM memory model (Reconciling High-level Optimizations and Low-level Code in LLVM, OOPSLA'18)
Language:Coq3 5 11
Ordinal
Language:Coq11 3 12
paco
A Coq library for parametric coinduction
Language:Coq43 7 2810
promising-coq
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
Language:Coq33 13 75

Software Foundations Laboratory's Repositories

snu-sf/paco
A Coq library for parametric coinduction
Language:Coq43 7 2810
snu-sf/promising-coq
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
Language:Coq33 13 75
snu-sf/crellvm
Crellvm: Verified Credible Compilation for LLVM
Language:Coq15 8 21
snu-sf/Ordinal
Language:Coq11 3 12
snu-sf/CompCertM
Language:Coq6 11 45
snu-sf/crellvm-llvm
LLVM for Crellvm: Verified Credible Compilation for LLVM
Language:C++6 7 00
snu-sf/CompCertR
Language:Coq4 9 14
snu-sf/llvmtwin-coq
Coq formalization of LLVM memory model (Reconciling High-level Optimizations and Low-level Code in LLVM, OOPSLA'18)
Language:Coq3 5 11
snu-sf/promising-arm
Language:Coq3 7 150
snu-sf/promising-ldrf-coq
The Coq development of local data-race-freedom guarantees in the Promising Semantics
Language:Coq3 4 00
snu-sf/clang-twin
LLVM implementation of OOSPLA'18 Reconciling High-level Optimizations and Low-level Code in LLVM
Language:C++2 5 0
snu-sf/fairness
Language:Coq2 1 54
snu-sf/promising2-coq
The Coq development of Promising 2.0 semantics for relaxed memory concurrency
Language:Coq2 4 01
snu-sf/CompCert
The CompCert C verified compiler
Language:Coq1 8 61
snu-sf/sflib
Language:Coq1 9 1210
snu-sf/snt
Show-and-tell Slides
1 16 01
snu-sf/promising-ir-coq
Language:Coq0 4 01
snu-sf/promising-seq-coq
The Coq development of PLDI'22 paper "Sequantial Reasoning for Optimizing Compilers under Weak Memory Concurrency"
Language:Coq0 6 01
snu-sf/sf-opam-coq-archive
0 3 02
snu-sf/coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Language:Coq0 01
snu-sf/CoreRUSC
Language:Coq4 0
snu-sf/HafniumCore
Language:Coq5 0
snu-sf/InteractionTrees
A Library for Representing Recursive and Impure Programs in Coq
Language:Coq1 01
snu-sf/llvm-twin
LLVM implementation of OOSPLA'18 Reconciling High-level Optimizations and Low-level Code in LLVM
Language:LLVM5 0
snu-sf/promising-ir-to-promising-arm
Language:Coq4 0
snu-sf/promising-lib
Language:Coq5 03
snu-sf/promising-opam-coq-archive
4 03
snu-sf/rusc
4 0
snu-sf/seminar-template
Language:TeX5 02
snu-sf/server-public
Language:Shell7 3