Very interesting to see the parallels between MacroML and Shen lisp Both support type-safe macros, both work in stages, and both have a small core language which the other stages are built on top of. The primary difference is that MacroML is based on CoreML, whereas Shen is based on klambda.

Does Shen have an equivalent to the formal semantics described in there that guarantee the properties they want? Or does it use its Sequent Calculus component for everything?

In Shen, types are defined in the notation of a single-conclusion sequent calculus. Sequent calculus has a long tradition in logic stemming from Gentzen’s foundational work in the area. It was taken up by many authors (e.g [6], [21]) to specify formal systems including type theories.

Cardelli L. Basic Polymorphic Type Checking, Science of Computer Programming, 1987.

Thompson S. Type Theory and Functional Programming, Addison-Wesley, 1991.

As I understand things, formal deduction is usually done in “Hilbert-style”, in which each additional assertion is an unconditional tautology. This is in contrast with “Gentzen-style”, in which each additional assertion is a conditional tautology. Sequent calculus is a Gentzen-style form, where each statement may have zero or more conditions. Everything I’m reading about it says sequent calculus is a “sound and complete” system of proof-making.

Im with you in not being formal enough to know. What Im trying to assess most is whether Shen’s is lower level and decidable like FOL or higher-level with more manual work like HOL. My initial guess was it’s more like the former given nature of how it’s used.

Very interesting to see the parallels between MacroML and Shen lisp Both support type-safe macros, both work in stages, and both have a small core language which the other stages are built on top of. The primary difference is that MacroML is based on CoreML, whereas Shen is based on klambda.

Does Shen have an equivalent to the formal semantics described in there that guarantee the properties they want? Or does it use its Sequent Calculus component for everything?

Is sequent calculus not formal enough? (Honest question, I don’t have much training in the way of formal methods.)

Poking around one of Mark Tarver’s more recent papers:

As I understand things, formal deduction is usually done in “Hilbert-style”, in which each additional assertion is an unconditional tautology. This is in contrast with “Gentzen-style”, in which each additional assertion is a conditional tautology. Sequent calculus is a Gentzen-style form, where each statement may have zero or more conditions. Everything I’m reading about it says sequent calculus is a “sound and complete” system of proof-making.

Im with you in not being formal enough to know. What Im trying to assess most is whether Shen’s is lower level and decidable like FOL or higher-level with more manual work like HOL. My initial guess was it’s more like the former given nature of how it’s used.