scientific article; zbMATH DE number 7204429

DOI10.4230/LIPICS.FSCD.2017.10MaRDI QIDQ5111306zbMATH OpenFDO

Authors Małgorzata Biernacka, Witold Charatonik, Klara Zielińska

Publication date 26 May 2020

zbMATH Keywords

Coqformal verificationabstract machinesreduction semantics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• From outermost reduction semantics to abstract machine
• From operational semantics to abstract machines
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
• A concrete framework for environment machines

Cites work

• scientific article; zbMATH DE number 1953288 (Why is no real title available?)
• A compiled implementation of strong reduction
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• A syntactic correspondence between context-sensitive calculi and abstract machines
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• An overview of the K semantic framework
• From outermost reduction semantics to abstract machine
• Functional runtime systems within the lambda-sigma calculus
• Lazy evaluation and delimited control
• Semantics engineering with PLT Redex
• Strongly reducing variants of the Krivine abstract machine
• Syntactic theories in practice

Cited in

(3)

• Deriving an abstract machine for strong call by need
• From outermost reduction semantics to abstract machine
• Automating the functional correspondence between higher-order evaluators and abstract machines

Describes a project that uses

Uses Software

• Coq
• K tool
• PLT Redex
• K Prover

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111306)