scientific article; zbMATH DE number 7204429

DOI10.4230/LIPIcs.FSCD.2017.10zbMath1441.68131MaRDI QIDQ5111306

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

Publication date: 26 May 2020

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

formal verificationreduction semanticsCoqabstract machines

Mathematics Subject Classification ID

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

Related Items (2)

Automating the functional correspondence between higher-order evaluators and abstract machines ⋮ Unnamed Item

Uses Software

• Coq
• K tool
• PLT Redex
• K Prover

Cites Work

• Unnamed Item
• Unnamed Item
• A syntactic correspondence between context-sensitive calculi and abstract machines
• An overview of the K semantic framework
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Strongly reducing variants of the Krivine abstract machine
• Syntactic Theories in Practice
• A compiled implementation of strong reduction
• From Outermost Reduction Semantics to Abstract Machine
• Functional runtime systems within the lambda-sigma calculus
• Lazy evaluation and delimited control
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy

This page was built for publication: