4 ms·
Shen (in particular its type system) is an executable Sequent Calculus system [0] written with a small portable lisp. This derives from a propositional logic sy
by emidln 10y ago
Shen (in particular its type system) is an executable Sequent Calculus system [0] written with a small portable lisp. This derives from a propositional logic system, not H-M over typed lambda calculus.
[0] - http://www.shenlanguage.org/learn-shen/types/types_sequent_calculus.html http://www.shenlanguage.org/learn-shen/types/types_sequent_c...
- jpt4 10y agoThank you for clarifying. Can you comment on the relative expressive power of Shen's type system versus e.g. Haskell? I understand that the former can accept as well-typed terms the other can't; in what way is this a consequence of modeling Shen's type system using the Sequent Calculus versus Hindley-Milner deduction?