Publication:4736387
From MaRDI portal
zbMath1054.68133MaRDI QIDQ4736387
Tobias Nipkow, Stefan Berghofer
Publication date: 9 August 2004
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2277/22770024.htm
Related Items
Two case studies of semantics execution in Maude: CCS and LOTOS, Proof synthesis and reflection for linear arithmetic, Partial and nested recursive function definitions in higher-order logic, Adapting functional programs to higher order logic, Verified bytecode verifiers., Verified bytecode verification and type-certifying compilation, Code-carrying theories, Turning Inductive into Equational Specifications, Formalizing the Logic-Automaton Connection, Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL, The Isabelle Framework
Uses Software