Published: 19th June 2016
DOI: 10.4204/EPTCS.213
ISSN: 2075-2180

EPTCS 213

Proceedings Sixth International Workshop on
Classical Logic and Computation
Porto, Portugal , 23th June 2016

Edited by: Ulrich Kohlenbach, Steffen van Bakel and Stefano Berardi

Preface
Ulrich Kohlenbach
On the Herbrand content of LK
Bahareh Afshari, Stefan Hetzl and Graham E. Leigh
1
Denotational Semantics of the Simplified Lambda-Mu Calculus and a New Deduction System of Classical Type Theory
Ken Akiba
11
The computational content of Nonstandard Analysis
Sam Sanders
24
A note on strong normalization in classical natural deduction
José Espírito Santo
41

Preface

The workshop series intends to cover research that investigates the computational aspects of classical logic and mathematics. Its focus is on unwinding the computational content of logical principles and proof in mathematics based on these principles, aiming to bring together researchers from both fields and exchange ideas.

Classical Logic and Computation (CL&C) 2016 was the sixth edition of this workshop series held as a satellite to FSCD 2016 on June 23, 2016 in Porto, Portugal.

In this sixth edition we received 11 submissions of both short and full papers. Eight (8) of these were selected to present at the meeting in Porto, and five (5) full papers were initially accepted to appear at this ETPCS special volume of which one was subsequently withdrawn by its authors.

An invited talk was given by Marc Bezem (U of Bergen): Coherent Logic - an overview.

Other topics covered by this years submissions included: computational content of proofs using nonstandard analysis, a structured grammar-based approach to the Herbrand content of proofs, semantics of the lambda-mu calculus, normalization of classical natural deduction proofs, t proof mining of noneffective proofs in convex optimization and algebra by functional interpretations.

I like to thank the members of the program committee for their excellent work:
Ulrich Kohlenbach (Darmstadt, PC Chair)