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