Sciweavers

CEFP
2009
Springer
13 years 4 months ago
Reasoning about Codata
Programmers happily use induction to prove properties of recursive programs. To show properties of corecursive programs they employ coinduction, but perhaps less enthusiastically. ...
Ralf Hinze
ENTCS
2007
105views more  ENTCS 2007»
13 years 6 months ago
Narrowing and Rewriting Logic: from Foundations to Applications
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 ...
Santiago Escobar, José Meseguer, Prasanna T...
ENTCS
2007
101views more  ENTCS 2007»
13 years 6 months ago
Semantic Determinism and Functional Logic Program Properties
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...
José Miguel Cleva, Francisco Javier L&oacut...
CADE
2010
Springer
13 years 7 months ago
iProver-Eq: An Instantiation-Based Theorem Prover with Equality
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...
Konstantin Korovin, Christoph Sticksel
ICDCS
2005
IEEE
13 years 12 months ago
Equational Approach to Formal Analysis of TLS
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...
Kazuhiro Ogata, Kokichi Futatsugi
HASKELL
2006
ACM
14 years 6 days ago
Introducing the Haskell equational reasoning assistant
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...
Andy Gill