LogicThe 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.
- 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.
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