17 search results for "tag:"category:Computer Science/Semantics and Compilation/Semantics""

Showing 1 - 17
  1. coq-compcert

    No documentation

    The CompCert C compiler (64 bit)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert date:2024-12-13
    Xavier Leroy
    3.15
    INRIA Non-Commercial License Agreement
    Used by 4 other packages
    03 Jan 2025
  2. coq-compcert-32

    No documentation

    The CompCert C compiler (32 bit)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert32 date:2023-07-04
    Xavier Leroy
    3.13.1
    INRIA Non-Commercial License Agreement
    Used by 1 other packages
    09 Nov 2023
  3. coq-compcert-64

    No documentation

    The CompCert C compiler (64 bit, using coq-platform supplied version of Flocq)
    category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:C keyword:compiler logpath:compcert64 date:2020-04-29
    Xavier Leroy
    3.7+8.12~coq_platform
    INRIA Non-Commercial License Agreement
    Used by 1 other packages
    28 Jul 2020
  4. coq-hoare-tut

    No documentation

    A Tutorial on Reflecting in Coq the generation of Hoare proof obligations
    category:Mathematics/Logic category:Computer Science/Semantics and Compilation/Semantics keyword:Hoare logic keyword:imperative program keyword:weakest precondition keyword:reflection logpath:HoareTut
    Sylvain Boulmé
    8.11.1
    LGPL-3.0-or-later
    Used by 0 other packages
    05 Jun 2020
  5. coq-katamaran

    No documentation

    Separation logic-based verification of instruction sets
    keyword:program verification keyword:separation logic keyword:symbolic execution keyword:instruction sets category:Computer Science/Semantics and Compilation/Semantics data:2022-07-19 logpath:Katamaran
    Dominique Devriese Georgy Lukyanov Sander Huyghebaert Steven Keuchel
    0.2.0
    BSD-2-Clause
    Used by 0 other packages
    21 Oct 2022
  6. coq-ott

    No documentation

    Auxiliary Coq library for Ott, a tool for writing definitions of programming languages and calculi
    category:Computer Science/Semantics and Compilation/Semantics keyword:abstract syntax logpath:Ott date:2024-12-30
    Peter Sewell Francesco Zappa Nardelli Scott Owens
    0.34
    BSD-3-Clause
    Used by 1 other packages
    30 Dec 2024
  7. coq-sail

    No documentation

    Support library for Sail, a language for describing the instruction semantics of processors
    logpath:Sail category:Computer Science/Semantics and Compilation/Semantics
    Alasdair Armstrong Thomas Bauereiss Brian Campbell Shaked Flur Jonathan French et al.
    0.19
    BSD-3-clause
    Used by 0 other packages
    14 Mar 2025
  8. coq-sail-stdpp

    No documentation

    Support library for Sail, a language for describing the instruction semantics of processors, using stdpp bitvectors
    logpath:Sail category:Computer Science/Semantics and Compilation/Semantics
    Alasdair Armstrong Thomas Bauereiss Brian Campbell Shaked Flur Jonathan French et al.
    0.19
    BSD-3-clause
    Used by 0 other packages
    14 Mar 2025
  9. coq-semantics

    No documentation

    A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation
    category:Computer Science/Semantics and Compilation/Semantics keyword:natural semantics keyword:denotational semantics keyword:axiomatic semantics keyword:Hoare logic keyword:Dijkstra weakest pre-condition calculus keyword:abstract interpretation keyword:intervals logpath:Semantics
    Yves Bertot
    8.14.0
    MIT
    Used by 0 other packages
    21 Nov 2021
  10. coq-smlms

    No documentation

    A formal semantics capturing value binding in a language with a powerful module system such as OCaml.
    category:Computer Science/Semantics and Compilation/Semantics keywords: adequacy keywords: modules keywords: module types keywords: OCaml keywords: refactoring keywords: renaming keywords: semantics logpath:AbstractRenaming date:2023-02-14
    Hugo Férée
    1.0.0
    MIT
    Used by 0 other packages
    16 Feb 2023
  11. coq-vellvm

    No documentation

    Coq library implementing (executable) semantics for LLVM IR
    date:2025-01-10 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm
    Steve Zdancewic <stevez@cis.upenn.edu> Yannick Zakowski <yannick.zakowski@inria.fr> Calvin Beck <hobbes@seas.upenn.edu> Irene Yoon <euisuny@cis.upenn.edu> Gary (Hanxi) Chen <hanxic@seas.upenn.edu>
    v2.0.20250110
    GPL-3.0-or-later
    Used by 0 other packages
    11 Jan 2025
  12. coq-vst

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-04-12
    Andrew W. Appel Lennart Beringer William Mansky Josiah Dodds Qinxiang Cao et al.
    3.0beta2
    BSD-2-Clause
    Used by 1 other packages
    15 Apr 2024
  13. coq-vst-32

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-03-20
    Andrew W. Appel Lennart Beringer Josiah Dodds Qinxiang Cao Aquinas Hobor et al.
    2.14
    BSD-2-Clause
    Used by 0 other packages
    21 Mar 2024
  14. coq-vst-64

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2020-08-02
    Andrew W. Appel Lennart Beringer Sandrine Blazy Qinxiang Cao Santiago Cuellar et al.
    2.6
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    03 Aug 2020
  15. coq-vst-iris

    No documentation

    Verified Software Toolchain with Iris
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2023-01-24
    William Mansky Shengyi Wang
    2.11.1
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    25 Jan 2023
  16. coq-wasm

    No documentation

    Wasm formalisation in Coq
    keyword:WebAssembly category:Computer Science/Semantics and Compilation/Semantics date:2025-03-13 logpath:Wasm
    Martin Bodin Philippa Gardner Jean Pichon Xiaojia Rao Conrad Watt
    2.0.2
    MIT
    Used by 0 other packages
    14 Mar 2025
  17. rocq-vellvm

    No documentation

    Rocq library implementing (executable) semantics for LLVM IR
    date:2025-03-27 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm
    Steve Zdancewic <stevez@cis.upenn.edu> Yannick Zakowski <yannick.zakowski@inria.fr> Calvin Beck <hobbes@seas.upenn.edu> Irene Yoon <euisuny@cis.upenn.edu> Gary (Hanxi) Chen <hanxic@seas.upenn.edu>
    v2.1.20250327
    GPL-3.0-or-later
    Used by 0 other packages
    27 Mar 2025