Skip to content

@snu-sf Software Foundations Laboratory

Change the repository type filter

All

    Repositories list

    44 repositories

    • sf-opam-coq-archive

      Public
      3•0•0•0•Updated Aug 8, 2025Aug 8, 2025

    • promising-lib

      Public
      Rocq Prover
      •
      BSD 2-Clause "Simplified" License
      •3•0•0•0•Updated Aug 8, 2025Aug 8, 2025

    • sflib

      Public
      Rocq Prover
      •
      BSD 2-Clause "Simplified" License
      •9•1•12•0•Updated Aug 8, 2025Aug 8, 2025

    • Ordinal

      Public
      Rocq Prover
      •
      MIT License
      •2•14•0•0•Updated Aug 3, 2025Aug 3, 2025

    • promising-arm

      Public
      Coq
      •
      BSD 2-Clause "Simplified" License
      •1•3•3•0•Updated Jul 31, 2025Jul 31, 2025

    • fairness

      Public
      Coq
      •4•4•1•1•Updated May 13, 2025May 13, 2025

    • CompCertR

      Public
      Coq
      •
      Other
      •4•4•0•2•Updated Mar 28, 2025Mar 28, 2025

    • CompCertM

      Public
      Coq
      •5•6•4•1•Updated Mar 27, 2025Mar 27, 2025

    • Archmage

      Public
      Coq
      •
      Other
      •0•1•0•0•Updated Jan 30, 2025Jan 30, 2025

    • paco

      Public
      A Coq library for parametric coinduction
      Coq
      •
      Other
      •11•50•2•1•Updated Jan 30, 2025Jan 30, 2025

    • promising-opam-coq-archive

      Public
      3•0•0•0•Updated Jan 21, 2025Jan 21, 2025

    • CompCert

      Public
      The CompCert C verified compiler
      Coq
      •
      Other
      •238•1•0•0•Updated Oct 20, 2024Oct 20, 2024

    • promising-coq

      Public
      The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
      concurrencyshared-memorypromising-semantics
      Coq
      •
      MIT License
      •5•40•4•0•Updated Oct 15, 2024Oct 15, 2024

    • promising-ir-to-promising-arm

      Public
      Coq
      •
      BSD 2-Clause "Simplified" License
      •0•0•0•0•Updated Aug 18, 2023Aug 18, 2023

    • promising2-coq

      Public
      The Coq development of Promising 2.0 semantics for relaxed memory concurrency
      concurrencypromising-semantics
      Coq
      •
      MIT License
      •1•2•0•1•Updated Jul 10, 2023Jul 10, 2023

    • promising-ir-coq

      Public
      Coq
      •1•0•0•0•Updated Mar 13, 2023Mar 13, 2023

    • promising-seq-coq

      Public
      The Coq development of PLDI'22 paper "Sequantial Reasoning for Optimizing Compilers under Weak Memory Concurrency"
      concurrencycompiler-optimizationpromising-semantics
      Coq
      •
      MIT License
      •1•0•0•0•Updated Nov 7, 2022Nov 7, 2022

    • promising-ldrf-coq

      Public
      The Coq development of local data-race-freedom guarantees in the Promising Semantics
      concurrencyshared-memorypromising-semantics
      Coq
      •
      MIT License
      •0•3•0•0•Updated Apr 9, 2022Apr 9, 2022

    • coq-ext-lib

      Public
      A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
      Coq
      •
      BSD 2-Clause "Simplified" License
      •50•0•0•0•Updated Apr 6, 2022Apr 6, 2022

    • InteractionTrees

      Public
      A Library for Representing Recursive and Impure Programs in Coq
      Coq
      •
      MIT License
      •54•0•0•1•Updated Mar 3, 2021Mar 3, 2021

    • server-public

      Public
      Shell
      •0•0•3•0•Updated Dec 17, 2020Dec 17, 2020

    • HafniumCore

      Public
      Coq
      •
      Apache License 2.0
      •0•0•0•0•Updated Jul 2, 2020Jul 2, 2020

    • rusc

      Public
      Apache License 2.0
      •0•0•0•0•Updated Jun 5, 2020Jun 5, 2020

    • CoreRUSC

      Public
      Coq
      •0•0•0•0•Updated May 26, 2020May 26, 2020

    • snt

      Public
      Show-and-tell Slides
      1•1•0•0•Updated Jun 3, 2019Jun 3, 2019

    • seminar-template

      Public
      TeX
      •2•0•0•0•Updated Mar 20, 2019Mar 20, 2019

    • llvmtwin-coq

      Public
      Coq formalization of LLVM memory model (Reconciling High-level Optimizations and Low-level Code in LLVM, OOPSLA'18)
      Coq
      •1•3•0•0•Updated Oct 19, 2018Oct 19, 2018

    • llvm-twin

      Public
      LLVM implementation of OOSPLA'18 Reconciling High-level Optimizations and Low-level Code in LLVM
      LLVM
      •
      Other
      •0•1•0•0•Updated Sep 8, 2018Sep 8, 2018

    • clang-twin

      Public
      LLVM implementation of OOSPLA'18 Reconciling High-level Optimizations and Low-level Code in LLVM
      C++
      •
      Other
      •0•3•0•0•Updated Aug 31, 2018Aug 31, 2018

    • crellvm

      Public
      Crellvm: Verified Credible Compilation for LLVM
      Coq
      •1•17•1•0•Updated Jun 26, 2018Jun 26, 2018