A complete semantics of \(\mathbb{K}\) and its translation to Isabelle

DOI10.1007/978-3-030-85315-0_10OpenAlexW3193631004MaRDI QIDQ2119971

Elsa L. Gunter, Liyi Li

Publication date: 31 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-85315-0_10

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items (1)

KtoIsabelle

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• LLVM
• Maude
• Toolchain
• K-Maude
• K-Java
• KJS
• GitHub
• Archive Formal Proofs
• K Prover
• LambdaMu-calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Order-sorted unification
• An overview of the K semantic framework
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Rewriting logic: Roadmap and bibliography
• Program verification by coinduction
• A modular order-sorted equational generalization algorithm
• Equational formulas and pattern operations in initial order-sorted algebras
• Mechanized semantics for the clight subset of the C language
• K-Java
• Verified Software Toolchain
• Towards a mechanized metatheory of standard ML
• A Declarative Language for the Coq Proof Assistant
• Run-time type computations in the Warren Abstract machine
• K-Maude: A Rewriting Based Tool for Semantics of Programming Languages
• All-Path Reachability Logic
• One-Path Reachability Logic
• An axiomatic basis for computer programming
• Logic of many-sorted theories

This page was built for publication: A complete semantics of \(\mathbb{K}\) and its translation to Isabelle