A systematic derivation of the STG machine verified in Coq

A systematic derivation of the STG machine verified in Coq

<p>Shared Term Graph (STG) is a lazy functional language used as an intermediate language in the Glasgow Haskell Compiler (GHC). In this article, we present a natural operational semantics for STG and we mechanically derive a lazy abstract machine from this semantics, which turns out to coinci...

पूर्ण विवरण

ग्रंथसूची विवरण
मुख्य लेखकों:	Pirog, M, Biernacki, D
स्वरूप:	Conference item
प्रकाशित:	ACM 2010

समान संसाधन

Formalising and Verifying Reference Attribute Grammars in Coq.
द्वारा: Schäfer, M, और अन्य
प्रकाशित: (2009)

Formalising and Verifying Reference Attribute Grammars in Coq
द्वारा: Schäfer, M, और अन्य
प्रकाशित: (2009)

ST Genesia reference values of 117 healthy donors measured with STG‐BleedScreen, STG‐DrugScreen and STG‐ThromboScreen reagents
द्वारा: Marisa Ninivaggi, और अन्य
प्रकाशित: (2021-01-01)

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
द्वारा: Burak Ekici, और अन्य
प्रकाशित: (2019-08-01)

Extracting and optimizing low-level bytecode from high-level verified Coq
द्वारा: Ioannidis, Eleftherios Ioannis.
प्रकाशित: (2019)

STG-ET: DLR Electric Propulsion Test Facility
द्वारा: Andreas Neumann
प्रकाशित: (2018-11-01)

STG-ET: DLR electric propulsion test facility
द्वारा: Andreas Neumann
प्रकाशित: (2017-04-01)

Sets in Coq, Coq in Sets
द्वारा: Bruno Barras
प्रकाशित: (2010-01-01)

Characterization of the Anti-HCV Activities of the New Cyclophilin Inhibitor STG-175.
द्वारा: Philippe A Gallay, और अन्य
प्रकाशित: (2016-01-01)

Translation Lookaside Buffer on the 65-nm STG DICE Hardened Elements
द्वारा: V. Ya. Stenin, और अन्य
प्रकाशित: (2018-06-01)

Formal Proof of a Machine Closed Theorem in Coq
द्वारा: Hai Wan, और अन्य
प्रकाशित: (2014-01-01)

CoqIOA : a formalization of IO automata in the Coq proof assistant
द्वारा: Athalye, Anish (Anish R.)
प्रकाशित: (2017)

STG-MTL: scalable task grouping for multi-task learning using data maps
द्वारा: Ammar Sherif, और अन्य
प्रकाशित: (2024-01-01)

A Machine Proof System of Point Geometry Based on Coq
द्वारा: Siran Lei, और अन्य
प्रकाशित: (2023-06-01)

STG i IFR-1 pri sakharnom diabete: rol' v patogeneze mikrososudistykh oslozhneniy
द्वारा: Natalya Nikitichna Volevodz, और अन्य
प्रकाशित: (2000-03-01)

Comparison Elements on STG DICE cell for Content-Addressable Memory and Simulation of Single-Event Transients
द्वारा: V. Ya. Stenin, और अन्य
प्रकाशित: (2017-06-01)

Single-cell activity in human STG during perception of phonemes is organized according to manner of articulation
द्वारा: Yair Lakertz, और अन्य
प्रकाशित: (2021-02-01)

Le coq médiéval
द्वारा: Michel Pastoureau
प्रकाशित: (2017-12-01)

Characterization of <i>Arabidopsis thaliana</i> Coq9 in the CoQ Biosynthetic Pathway
द्वारा: Mei Hu, और अन्य
प्रकाशित: (2023-06-01)

Human COQ9 Rescues a coq9 Yeast Mutant by Enhancing Coenzyme Q Biosynthesis from 4-Hydroxybenzoic Acid and Stabilizing the CoQ-Synthome
द्वारा: Cuiwen H. He, और अन्य
प्रकाशित: (2017-07-01)

Emergence of a Streptococcus dysgalactiae subspecies equisimilis stG62647-lineage associated with severe clinical manifestations
द्वारा: Oddvar Oppegaard, और अन्य
प्रकाशित: (2017-08-01)

Machine−Verifiable Responsiveness
द्वारा: Roscoe, A, और अन्य
प्रकाशित: (2005)

Deciding Kleene Algebras in Coq
द्वारा: Thomas Braibant, और अन्य
प्रकाशित: (2012-03-01)

CoQ10 and Aging
द्वारा: Isabella Peixoto de Barcelos, और अन्य
प्रकाशित: (2019-05-01)

PIDE for Asynchronous Interaction with Coq
द्वारा: Carst Tankink
प्रकाशित: (2014-10-01)

stg fimbrial operon from S. Typhi STH2370 contributes to association and cell disruption of epithelial and macrophage-like cells
द्वारा: Liliana Berrocal, और अन्य
प्रकाशित: (2015-01-01)

Encephalopathy, kidney failure and retinopathy. CoQ10 deficiency due to COQ8B mutation
द्वारा: Victor Adam Lancet, और अन्य
प्रकाशित: (2021-06-01)

Transmission Electron Microscopy Data on drusen-like deposits in the retinal degeneration sTg-IRBP: HEL mouse model
द्वारा: Yi-Hsia Liu, और अन्य
प्रकाशित: (2019-02-01)

Computable analysis and notions of continuity in Coq
द्वारा: Florian Steinberg, और अन्य
प्रकाशित: (2021-05-01)

An introduction to small scale reflection in Coq
द्वारा: Georges Gonthier, और अन्य
प्रकाशित: (2010-01-01)

Manganese-driven CoQ deficiency
द्वारा: Jutta Diessl, और अन्य
प्रकाशित: (2022-10-01)

Formalization of Quantum Protocols using Coq
द्वारा: Jaap Boender, और अन्य
प्रकाशित: (2015-11-01)

LF+ in Coq for "fast and loose" reasoning
द्वारा: Fabio Alessi, और अन्य
प्रकाशित: (2019-12-01)

Enseñando métodos formales con Coq
द्वारा: Carlos Daniel Luna
प्रकाशित: (2006-12-01)

Enseñando métodos formales con Coq
द्वारा: Luna, Carlos Daniel
प्रकाशित: (2006-01-01)

Correct-by-construction finite field arithmetic in Coq
द्वारा: Philipoom, Jade (Jade D.)
प्रकाशित: (2018)

A Functional Derivation of the Warren Abstract Machine
द्वारा: Pirog, M, और अन्य
प्रकाशित: (2011)

Novel recessive mutations in COQ4 cause severe infantile cardiomyopathy and encephalopathy associated with CoQ10 deficiency
द्वारा: Neal Sondheimer, और अन्य
प्रकाशित: (2017-09-01)

A reflection−based proof tactic for lattices in Coq
द्वारा: James, D, और अन्य
प्रकाशित: (2010)

A reflection−based proof tactic for lattices in Coq
द्वारा: James, D, और अन्य
प्रकाशित: (2009)