Ebook: Logic from Computer Science: Proceedings of a Workshop held November 13–17, 1989

The volume is the outgrowth of a workshop with the same title held at MSRI in the week of November 13-17, 1989, and for those who did not get it, Logic from Computer Science is the converse of Logic in Computer Science, the full name of the highly successful annual LICS conferences. We meant to have a conference which would bring together the LICS commu­ nity with some of the more traditional "mathematical logicians" and where the emphasis would be on the flow of ideas from computer science to logic rather than the other way around. In a LICS talk, sometimes, the speaker presents a perfectly good theorem about (say) the A-calculus or finite model theory in terms of its potential applications rather than its (often more ob­ vious) intrinsic, foundational interest and intricate proof. This is not meant to be a criticism; the LICS meetings are, after all, organized by the IEEE Computer Society. We thought, for once, it would be fun to see what we would get if we asked the speakers to emphasize the relevance of their work for logic rather than computer science and to point out what is involved in the proofs. I think, mostly, it worked. In any case, the group of people represented as broad a selection of logicians as I have seen in recent years, and the quality of the talks was (in my view) exceptionally, unusually high. I learned a lot and (I think) others did too.

---

Topics of this proceedings volume will include Computability and Complexity of Higher Type Functions by Stephen Cook, Logics for Termination and Correctness of Functional Programs by Solomon Feferman, Reals and Forcing with Elementary Topos by the well known mathematician, Saunders MacLane and Ieke Moerdijk, and Concurrent Computation as Game Playing by Anil Nerode.

---

Topics of this proceedings volume will include Computability and Complexity of Higher Type Functions by Stephen Cook, Logics for Termination and Correctness of Functional Programs by Solomon Feferman, Reals and Forcing with Elementary Topos by the well known mathematician, Saunders MacLane and Ieke Moerdijk, and Concurrent Computation as Game Playing by Anil Nerode.
Content:
Front Matter....Pages i-xi
The Imperative Future: Past Successes ? Future Actions....Pages 1-16
A Logical Operational Semantics of Full Prolog: Part III. Built-In Predicates for Files, Terms, Arithmetic and Input-Output....Pages 17-50
Computability and Complexity of Higher Type Functions....Pages 51-72
Constructively Equivalent Propositions and Isomorphisms of Objects, or Terms as Natural Transformations....Pages 73-94
Logics for Termination and Correctness of Functional Programs....Pages 95-127
Transparent Grammars....Pages 129-151
Designing Unification Procedures Using Transformations: A Survey....Pages 153-215
Normal Forms and Cut-Free Proofs as Natural Transformations....Pages 217-241
Computer Implementation and Applications of Kleene’s S-M-N and Recursion Theorems....Pages 243-263
0–1 Laws for Fragments of Second-Order Logic: An Overview....Pages 265-286
No Counter-Example Interpretation and Interactive Computation....Pages 287-293
Semantic Characterizations of Number Theories....Pages 295-317
Constructive Kripke Semantics and Realizability....Pages 319-357
Splitting and Density for the Recursive Sets of a Fixed Time Complexity....Pages 359-372
Reals and Forcing with an Elementary Topos....Pages 373-385
Completeness Theorems for Logics of Feature Structures....Pages 387-403
Concurrent Programs as Strategies in Games....Pages 405-479
Finite and Infinite Dialogues....Pages 481-497
Some Relations Between Subsystems of Arithmetic and Complexity of Computations....Pages 499-519
Logics for Negation as Failure....Pages 521-583
Normal Varieties of Combinators....Pages 585-596
Complexity of Proofs in Classical Propositional Logic....Pages 597-608

---

Topics of this proceedings volume will include Computability and Complexity of Higher Type Functions by Stephen Cook, Logics for Termination and Correctness of Functional Programs by Solomon Feferman, Reals and Forcing with Elementary Topos by the well known mathematician, Saunders MacLane and Ieke Moerdijk, and Concurrent Computation as Game Playing by Anil Nerode.
Content:
Front Matter....Pages i-xi
The Imperative Future: Past Successes ? Future Actions....Pages 1-16
A Logical Operational Semantics of Full Prolog: Part III. Built-In Predicates for Files, Terms, Arithmetic and Input-Output....Pages 17-50
Computability and Complexity of Higher Type Functions....Pages 51-72
Constructively Equivalent Propositions and Isomorphisms of Objects, or Terms as Natural Transformations....Pages 73-94
Logics for Termination and Correctness of Functional Programs....Pages 95-127
Transparent Grammars....Pages 129-151
Designing Unification Procedures Using Transformations: A Survey....Pages 153-215
Normal Forms and Cut-Free Proofs as Natural Transformations....Pages 217-241
Computer Implementation and Applications of Kleene’s S-M-N and Recursion Theorems....Pages 243-263
0–1 Laws for Fragments of Second-Order Logic: An Overview....Pages 265-286
No Counter-Example Interpretation and Interactive Computation....Pages 287-293
Semantic Characterizations of Number Theories....Pages 295-317
Constructive Kripke Semantics and Realizability....Pages 319-357
Splitting and Density for the Recursive Sets of a Fixed Time Complexity....Pages 359-372
Reals and Forcing with an Elementary Topos....Pages 373-385
Completeness Theorems for Logics of Feature Structures....Pages 387-403
Concurrent Programs as Strategies in Games....Pages 405-479
Finite and Infinite Dialogues....Pages 481-497
Some Relations Between Subsystems of Arithmetic and Complexity of Computations....Pages 499-519
Logics for Negation as Failure....Pages 521-583
Normal Varieties of Combinators....Pages 585-596
Complexity of Proofs in Classical Propositional Logic....Pages 597-608
....