Quick specifications for the busy programmer

DOI10.1017/S0956796817000090zbMath1418.68037OpenAlexW2559071439WikidataQ114116626 ScholiaQ114116626MaRDI QIDQ5371995

Moa Johansson, Nicholas Smallbone, Koen Claessen, Maximilian Algehed

Publication date: 23 October 2017

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796817000090

zbMATH Keywords

Haskelltheory exploration

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Theory exploration powered by deductive synthesis ⋮ Automated theory exploration for interactive theorem proving: an introduction to the Hipster system ⋮ Into the Infinite - Theory Exploration for Coinduction ⋮ Abstract Contract Synthesis and Verification in the Symbolic 𝕂 Framework

Uses Software

• Theorema
• Haskell
• Daikon
• QuickCheck
• HipSpec
• Hipster
• QuickSpec
• IsaCoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Zur Struktur von Alternativkörpern
• Functional geometry
• The Daikon system for dynamic detection of likely invariants
• The octonions
• Automating Inductive Proofs Using Theory Exploration
• Hipster: Integrating Theory Exploration in a Proof Assistant