UTPCalc — A Calculator for UTP Predicates

DOI10.1007/978-3-319-52228-9_10zbMath1483.68072OpenAlexW2570848523MaRDI QIDQ2971182

Andrew Butterfield

Publication date: 4 April 2017

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/10344/5665

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (1)

Theoretical and practical approaches to the denotational semantics for MDESL based on UTP

Uses Software

• Coq
• Stratego
• Isabelle/HOL
• Isabelle/Isar
• PVS
• Haskell
• Isar
• Maude
• Saoithin
• UTP2
• Isabelle/UTP
• UTPCalc

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle/HOL. A proof assistant for higher-order logic
• Isabelle/UTP: A Mechanised Theory Engineering Framework
• Saoithín: A Theorem Prover for UTP
• The Logic of U ·(TP)2
• Mechanical Reasoning about Families of UTP Theories
• Mechanising a Unifying Theory

This page was built for publication: UTPCalc — A Calculator for UTP Predicates