------------------------------------------------------------------------- 
------------------------------------------------------------------------- 
CL&C 2016 SCHEDULE
------------------------------------------------------------------------- 
------------------------------------------------------------------------- 
 09:00 - 10:00 Marc Bezem: 
 Coherent Logic – an overview (invited talk) 

 ------------------------------------------------------------------ 
 10:00 - 10:30 (coffe break) 
 ------------------------------------------------------------------ 
 
 10:30 - 10:55 Federico Aschieri: 
 Natural Deduction and Curry-Howard for Herbrand Constructive Logics 

 
 10:55 - 11:45 Sam Sanders 
 The computational content of Nonstandard Analysis 

 11:45 - 12:10 Daniel Koernlein 
 Proof Mining in Nonlinear Analysis 

 12:10 - 12:35 Thomas Powell 
 The computational content of Zorn's lemma 
 ------------------------------------------------------------------ 
 12:35 - 14:00 (lunch break) 
 ------------------------------------------------------------------ 
 14:00 - 14:50 Ken Akiba 
 Denotational semantics of the simplified lambda-mu calculus and a new deduction system of classical type theory 
 14:50 - 15:40 Hugo Herbelin and Étienne Miquey 
 A continuation-passing-style interpretation of simply-typed call-by-need lambda-calculus with control within System F 
 ------------------------------------------------------------------ 
 15:40 - 16:20 (coffee break) 
 ------------------------------------------------------------------ 
 16:20 - 17:10 José Espírito Santo 
 A note on strong normalization in classical natural deduction 
 17:10 – 18:00 Bahareh Afshari, Stefan Hetzl and Graham Leigh 
 On the Herbrand content of LK 
------------------------------------------------------------------ 
------------------------------------------------------------------ 
 ABSTRACT
------------------------------------------------------------------ 
Marc Bezem: Coherent Logic – an overview (invited talk) 
------------------------------------------------------------------
Coherent logic (CL) is a fragment of first-order logic that is more expressive than resolution logic in that it allows a restricted form of existential quantification. Consequently, many theories can be formulated directly in CL, in particular without skolemization. CL has a simple proof theory yielding readable proofs. Thus it strikes a balance beween expressivity and efficiency of automated reasoning. In the talk we give an overview of various aspects of CL. 
------------------------------------------------------------------