6 citations · 6 across the 2 of their papers we have counts for
4 papers · 1 filter
Operationally-based Program Equivalence Proofs using LCTRSs
Ştefan Ciobâcă, Dorel Lucanu, Andrei Sebastian Buruiană
We propose an operationally-based deductive proof method for program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LC…
Unification in Matching Logic - Extended Version
Andrei Arusoaie, Dorel Lucanu
Matching Logic is a framework for specifying programming language semantics and reasoning about programs. Its formulas are called patterns and are built with variables, symbols, co…
A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems
Ştefan Ciobâcă, Dorel Lucanu
We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-s…
Automatic Equivalence Proofs for Non-deterministic Coalgebras
Marcello Bonsangue, Georgiana Caltais, Eugen-Ioan Goriac +3
A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analogue of Kleene's theorem and Kleene algebra, were recently proposed by a…