Standardized notation can be helpful, especially after a topic has matured. For example, Gentzen used as an infix symbol to build sequents from lists of formulas. While one also sees used, it seems that in recent years, has become the standard, especially when proof theory is applied to type theory (where is invariably used) and…
Dale Miller
I received my Ph.D. in Mathematics in 1983 from Carnegie Mellon University. I have been a professor at the University of Pennsylvania and Ecole Polytechnique (France) and Department Head in Computer Science and Engineering at Pennsylvania State University. I am currently a Director of Research at Inria Saclay. My research interests include various topics in computational logic including proof theory, automated reasoning, logic programming, unification theory, operational semantics, and proof certificates.
LK vs LJ: An origin story for linear logic
In his 1987 TCS paper [2], Girard credits semantic considerations related to coherent models as the origin of the key observation behind linear logic: the intuitionistic implication should be split into two connectives . To the extent that it makes sense to propose an alternative origin story for linear logic, it is interesting to note…
