Skip to content

@snu-sf Software Foundations Laboratory

Change the repository type filter

All

    Repositories list

    44 repositories

    • fairness

      Public
      Coq
      •4•2•1•1•Updated Dec 9, 2024Dec 9, 2024

    • Archmage

      Public
      Coq
      •
      Other
      •0•1•0•0•Updated Nov 19, 2024Nov 19, 2024

    • CompCert

      Public
      The CompCert C verified compiler
      Coq
      •
      Other
      •230•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•33•4•0•Updated Oct 15, 2024Oct 15, 2024

    • paco

      Public
      A Coq library for parametric coinduction
      Coq
      •
      Other
      •10•43•2•0•Updated Oct 9, 2024Oct 9, 2024

    • promising-arm

      Public
      Coq
      •
      BSD 2-Clause "Simplified" License
      •0•3•3•0•Updated Oct 4, 2024Oct 4, 2024

    • promising-lib

      Public
      Coq
      •3•0•0•0•Updated Oct 4, 2024Oct 4, 2024

    • Ordinal

      Public
      Coq
      •
      MIT License
      •2•11•0•0•Updated Sep 26, 2024Sep 26, 2024

    • sf-opam-coq-archive

      Public
      2•0•0•0•Updated Jan 12, 2024Jan 12, 2024

    • sflib

      Public
      Coq
      •10•1•12•0•Updated Jan 12, 2024Jan 12, 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-opam-coq-archive

      Public
      3•0•0•0•Updated Mar 13, 2023Mar 13, 2023

    • CompCertR

      Public
      Coq
      •
      Other
      •4•4•0•2•Updated Feb 25, 2023Feb 25, 2023

    • CompCertM

      Public
      Coq
      •5•6•4•1•Updated Feb 25, 2023Feb 25, 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
      •46•0•0•0•Updated Apr 6, 2022Apr 6, 2022

    • InteractionTrees

      Public
      A Library for Representing Recursive and Impure Programs in Coq
      Coq
      •
      MIT License
      •51•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•15•1•0•Updated Jun 26, 2018Jun 26, 2018