CEFP
2009
Springer
13 years 9 months ago
2009
Springer
Programmers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. ...
ENTCS
2007
13 years 11 months ago
2007
Narrowing was originally introduced to solve equational E-unification problems. It has also been recognized as a key mechanism to unify functional and logic programming. In both ...
ENTCS
2007
13 years 11 months ago
2007
In modern functional logic languages like Curry or Toy, programs are possibly non-confluent and nonterminating rewrite systems, defining possibly non-deterministic non-strict fu...
CADE
2010
Springer
14 years 17 days ago
2010
Springer
iProver-Eq is an implementation of an instantiation-based calculus Inst-Gen-Eq which is complete for first-order logic with equality. iProver-Eq extends the iProver system with sup...
ICDCS
2005
IEEE
14 years 5 months ago
2005
IEEE
TLS has been formally analyzed with the OTS/CafeOBJ method. In the method, distributed systems are modeled as transition systems, which are written in terms of equations, and it i...
HASKELL
2006
ACM
14 years 5 months ago
2006
ACM
We introduce the new, improved version of the Haskell Equational Reasoning Assistant, which consists of an Ajax application for rewriting Haskell fragments in their context, and a...