scientific article; zbMATH DE number 2003148

zbMath1023.68021MaRDI QIDQ4435458

Stefan Berghofer

Publication date: 12 November 2003

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2646/26460021.htm

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Flyspeck II: The basic linear programs, A realizability interpretation of Church's simple theory of types, Intuitionistic fixed point logic, A mechanized proof of the basic perturbation lemma, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Generating certified code from formal proofs: a case study in homological algebra, Two case studies of semantics execution in Maude: CCS and LOTOS, Program extraction from normalization proofs

Uses Software

• Isabelle
• Isabelle/HOL
• Isabelle/Isar
• HOL-OCL
• ETPS
• Nuprl