Software Foundations Laboratory

Seoul, Korea

Pinned Repositories

CompCertM
Language:Coq6 10 45
CompCertR
Language:Coq4 8 14
crellvm
Crellvm: Verified Credible Compilation for LLVM
Language:Coq13 8 21
crellvm-llvm
LLVM for Crellvm: Verified Credible Compilation for LLVM
Language:C++5 7 00
llvm-freeze
Language:LLVM4 18 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 2 12
paco
A Coq library for parametric coinduction
Language:Coq41 9 2710
promising-coq
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
Language:Coq32 13 75
promising-ldrf-coq
The Coq development of local data-race-freedom guarantees in the Promising Semantics
Language:Coq3 4 00

Software Foundations Laboratory's Repositories

snu-sf/paco
A Coq library for parametric coinduction
Language:Coq41 9 2710
snu-sf/promising-coq
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
Language:Coq32 13 75
snu-sf/crellvm
Crellvm: Verified Credible Compilation for LLVM
Language:Coq13 8 21
snu-sf/Ordinal
Language:Coq11 2 12
snu-sf/CompCertM
Language:Coq6 10 45
snu-sf/crellvm-llvm
LLVM for Crellvm: Verified Credible Compilation for LLVM
Language:C++5 7 00
snu-sf/CompCertR
Language:Coq4 8 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 15
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/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/fairness
Language:Coq1 1 53
snu-sf/sf-opam-coq-archive
1 3 02
snu-sf/sflib
Language:Coq1 8 1210
snu-sf/snt
Show-and-tell Slides
1 15 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 00
snu-sf/coq-ext-lib
A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
Language:Coq0 0
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-coq
Language:Coq4 01
snu-sf/promising-ir-to-promising-arm
Language:Coq4 0
snu-sf/promising-lib
Language:Coq5 02
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