scientific article; zbMATH DE number 7204429

DOI10.4230/LIPICS.FSCD.2017.10zbMATH Open1441.68131MaRDI QIDQ5111306FDOQ5111306

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

Publication date: 26 May 2020

Title of this publication is not available (Why is that?)

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

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)

Cites Work

• An overview of the K semantic framework
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• A syntactic correspondence between context-sensitive calculi and abstract machines
• Syntactic theories in practice
• Semantics engineering with PLT Redex
• Lazy evaluation and delimited control
• Strongly reducing variants of the Krivine abstract machine
• A compiled implementation of strong reduction
• Functional runtime systems within the lambda-sigma calculus
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• From Outermost Reduction Semantics to Abstract Machine
• Title not available (Why is that?)

Cited In (2)

• Title not available (Why is that?)
• Automating the functional correspondence between higher-order evaluators and abstract machines

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)