A Semi-reflexive Tactic for (Sub-)Equational Reasoning

2006 ◽  
pp. 98-114 ◽  
Author(s):  
Claudio Sacerdoti Coen
Keyword(s):  
Equational Reasoning

scholarly journals Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs

2016 ◽  
Vol 50 (12) ◽  
pp. 23-34 ◽  
Author(s):  
Andrew Farmer ◽  
Neil Sculthorpe ◽  
Andy Gill
Keyword(s):  
Tool Support ◽  
Equational Reasoning

Equational reasoning about nondeterministic processes

1990 ◽  
Vol 2 (1) ◽  
pp. 167-195 ◽  
Author(s):  
Jayadev Misra
Keyword(s):  
Equational Reasoning

A Calculus for (Meta)Models and Transformations

2014 ◽  
Vol 24 (05) ◽  
pp. 715-730 ◽  
Author(s):  
Laurent Thiry ◽  
Michel Hassenforder
Keyword(s):  
Category Theory ◽  
Point Of View ◽  
Modeling Languages ◽  
Formal Representation ◽  
Equational Reasoning ◽  
Natural Transformations ◽  
Formal Point

This paper proposes a formal representation of modeling languages based on category theory. These languages are generally described by "metamodels", i.e. structures composed by classes and relations, and related by "transformations". Thus, this paper studies how the key categorical concepts such as functors and relations between functors (called natural transformations) can be used for equational reasoning about modeling artifacts (models, metamodels, transformations). As a result, this paper proposes a formal point of view of models usable to specify/prove equivalence between models or transformations (with an application to refactoring).

Concrete stream calculus: An extended study

2010 ◽  
Vol 20 (5-6) ◽  
pp. 463-535 ◽  
Author(s):  
RALF HINZE
Keyword(s):  
Generating Functions ◽  
Proof Technique ◽  
Extended Study ◽  
Equational Reasoning ◽  
The Rich ◽  
Infinite Sequences

AbstractThis paper shows how to reason about streams concisely and precisely. Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive datatype, operations on streams are implemented by corecursive programs, and proofs are typically concocted using coinduction. This paper offers an alternative to coinduction. Suitably restricted, stream equations possessunique solutions. This property gives rise to a simple and attractive proof technique, essentially bringing equational reasoning to the coworld. We redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators, building on the cornerstone of unique solutions. The paper contains a smörgåsbord of examples: we study recursion elimination, investigate the binary carry sequence, explore Sprague-Grundy numbers and present two proofs of Moessner's Theorem. The calculations benefit from the rich structure of streams. As the type of streams is an applicative functor we can effortlessly lift operations and their properties to streams. In combination with Haskell's facilities for overloading, this greatly contributes to conciseness of notation. The development is indeed constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use.

Sign in / Sign up

Export Citation Format

Share Document