scientific article; zbMATH DE number 2085164

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

Related Items

Verified bytecode verifiers. ⋮ Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs ⋮ Verified bytecode verification and type-certifying compilation ⋮ Verified Root-Balanced Trees ⋮ Turning Inductive into Equational Specifications ⋮ Formalizing the Logic-Automaton Connection ⋮ Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL ⋮ Code-carrying theories ⋮ Proof Pearl: regular expression equivalence and relation algebra ⋮ Introduction to ``Milestones in interactive theorem proving ⋮ Extracting functional programs from Coq, in Coq ⋮ Unnamed Item ⋮ A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL ⋮ The Isabelle Framework ⋮ Proof synthesis and reflection for linear arithmetic ⋮ Partial and nested recursive function definitions in higher-order logic ⋮ From LCF to Isabelle/HOL ⋮ A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl) ⋮ Isabelle's metalogic: formalization and proof checker ⋮ Adapting functional programs to higher order logic ⋮ A formalization and proof checker for Isabelle's metalogic ⋮ A formalisation of the Myhill-Nerode theorem based on regular expressions ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS

Uses Software