SEQUEL (SEQUEnt processing Language) was the ancestor of Shen and was introduced in 1992 in The Sixth International Conference on Symbolic and Logical Computing. SEQUEL was designed from the outset as a shell in which logic rules could be entered directly as sequent rules. Unlike the LCF and the LF, SEQUEL was a programming language in its own right; sequent rules were used to describe type theories which were used to typecheck SEQUEL programs.
SEQUEL was to evolve into Qi in 2005 which became Shen in 2011. The essential ideas remained the same, though the realisation of those ideas became steadily more sophisticated over a 30 year period. During that period, the focus of direction for SEQUEL/Qi/Shen moved from representing logics to programming in general and Qi was even used to model transport systems.
By the time of Shen, the focus was entirely on general purpose programming. In this respect, Shen followed the trajectory of ML, which began life as a support language for programming proof strategies in the LCF and ended as a general purpose programming language in the shape of Standard ML.
Qi, introduced in 2005 and published in 2008 was the last version of my work to include inbuilt provision for the representation of arbitrary logical systems and an inbuilt proof assistant for executing proofs. In 2011 Shen left this feature completely behind.
In 2021 I began to reflect that this application area should be brought back by some form of library code. Thus was born the Logic Lab, which combined the modern resources of Shen with the ability to frame logical systems directly in terms of sequent rules. The Logic Lab benefited greatly from the 30 year gap between SEQUEL and the latest S30 Shen kernel that I was using in 2021.
Not only does the Logic Lab generate highly efficient code from sequent calculus, but this code is automatically proved to be type secure wrt the syntax of the logic in question. The Logic Lab also solves certain awkward questions (that I had not solved in 1992) about formalising sequent rules with unusual side conditions (we'll see some of those later) and best of all – it doesd all this in less than 500 lines of Shen!
Mark
To view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/CACnPB4ou0rc5Q%2B%2Brp0-C8t5kDeBmqpHXWtiV%3DR%2BJpAKkLDmwpQ%40mail.gmail.com.