CTO CLiki for the TUNES project

Home About CLiki Text Formatting

Logic

The term for a paradigm of programming that originates in the Curry-Howard Isomorphism, which relates types and proofs to terms and expressions. In most cases, logical deduction or inference is equated with term evaluation or state update.

• The Association for Logic Programming (ALP).
• Logic Programming at The WWW Virtual Library.
• logic-programming.org actually empty.
• Formal logic via functional programming: a dissertation.
• Termination inference, a kind of program analysis for logic programs.

• Schelog3 [MIA].
• SPIKE. From its readme:

  The SPIKE system is an automatic theorem prover in theories presented by conditional equations. SPIKE was written in Caml Light, a functional language of the ML family.

---

Pages in this topic: ALF   ASF+SDF   Axiom of Choice   CafeOBJ   Claire   Curry   Curry-Howard Isomorphism   Dynamo   Escher   Goedel   Lambda Prolog   LIFE   Maude   Mercury   NuPrl   Prolog   SPARCL   TyRuBa   Yarrow  

---

Also linked from: Actor   Alan Bundy   BOBJ   Constraints   Declarative   Fifth Generation Computer Systems   Induction and Co-induction   Janus   NCL   OBJ Family   Quotienting   Referential Transparency and State   Scheme   Unification