PCC 2013 Accepted Papers with Abstracts

Joseph Boudou and Bruno Woltzenlogel Paleo. Compression of Propositional Resolution Proofs by Lowering Subproofs
Abstract: In this talk we will describe a new propositional resolution proof compression algorithm generalizing LowerUnits and called LowerUnivalents. By lowering more subproofs, this algorithm is able to compress more than LowerUnits. Moreover, its design allows to implement a non-sequential combination of LowerUnivalents after RecyclePivotsWithIntersection resulting in a fast and efficient propositional resolution proof compression algorithm.
Nicolas Guenot. On the computational interpretation of contraction in deep inference
Abstract: The work-in-progress presented here focuses on the handling of contraction in the setting of deep inference, and in particular in the calculus of structures, and how it can impact the design of functional calculi through a correspondence established by a type system. The general form of contraction in a system for intuitionistic logic provides more possibilities in the structure of proofs and therefore allows to write extended lambda-terms where resources are handled in a refined way: exploring the computational interpretations of variants of the contraction rule gives interesting insights on the duplication and sharing of terms and computations.
Hugo Herbelin, Gyesik Lee and Keiko Nakata. Computational interpretation for the big five systems of reverse mathematics
Abstract: The goal of (classical) reverse mathematics is to assess the logical
strength underlying theorems of ordinary non-set-theoretic
mathematics. Simpson describes five basic subsystems of the second
order arithmetic, called the big five systems. These subsystems
differ primarily in their set comprehension axioms, which assert what
sets must exist. Many theorems from ordinary mathematics turn out to
be equivalent to one of these subsystems on the needed strength of set
existence axioms. In this talk, I will present our ongoing project
aiming at providing computational interpretation for the big five
systems by Curry-Howard correspondence.
Susumu Yamasaki. Algebraic Compositions of Action Structures for Function Terms
Abstract: With a motivation of modeling mobile device functions by state-constraint lambda terms, this talk presents an action structure which contains recursion of action applications with communication facilities. For action semantics with respect to distributed computing, this topic is concerned with a distributed action structure
consisting of rule sets including defaults, as well as with algebraic compositions
of rule sets. As behavioral aspects of the action structure, implementation and default of actions are denoted by some fixed point of a mapping associated with a given action structure. Each action is devoted to state-transitions in a state-constraint function conversion system as a mobile device model. This talk also contains some algebraic aspect of action structures, by which recursion and communication included in action structures can be viewed and represented.
Reinhard Kahle and Anton Setzer. The extended predicative Mahlo universe in explicit mathematics
Abstract: The Mahlo universe has been introduced in order to obtain
a predicatively justified proof theoretically strong
extension of Martin-Loef Type Theory. The strength is of this
theory is Kripke-Platek set theory extended by one recursively
Mahlo ordinal and finitely many admissibles above it,
and therefore it proves the extension of for instance
the theory KPM.

There have been many discussions in the proof theoretic
community whether this theory is indeed predicatively
justified. In this talk we present the extended predicative
Mahlo universe in the setting of explicit mathematics.
This Mahlo universe is entirely built from below and can
therefore be considered as predicatively justified.
The ordinary Mahlo universe in explicit mathematics
can easily be embedded into this theory and therefore
it is likely to be slightly stronger than the Mahlo
universe in type theory.

We will introduce this theory and show how to adapt
the model construction in an article by Jaeger and Studer
in order to obtain a model for the extended predicative Mahlo
Universe.
James Chapman, Tarmo Uustalu and Niccolò Veltri. Formalizing restriction categories
Abstract: Inspired by the course that Robin Cockett gave this winter in Tallinn, we undertook to formalize restriction categories in Agda.

Restriction categories are an abstract framework by Robin Cockett and Steve Lack for reasoning partiality. They are complete with respect to some more concrete frameworks such as partial map categories and partial map classifiers. A specialization of restriction categories, Turing categories, by Robin Cockett and Pieter Hofstra, is an abstract framework for computability and also for complexity.

The aim of this work is to see if the highly modular organization of the theory of restriction categories can be used to build a practical infrastructure for supporting programming with partial functions in dependently typed programming languages such as Agda.
Danko Ilik and Keiko Nakata. A Direct Constructive Proof of Open Induction on Cantor Space
Abstract: Open Induction (OI) is a principle classically equivalent to Dependent
Choice, which is, unlike the later, closed under double-negation
translation and A-translation. In the context of Constructive Reverse
Mathematics, Wim Veldman has shown that, in presence of Markov's
Principle, OI on Cantor space is equivalent to Double-negation Shift.
We rework on Veldman's proof to give a direct constructive
proof of OI on Cantor space in a constructive intermediate logic based
on delimited control operators.
Martin Sticht. A Game-Theoretic Decision Procedure for the Constructive Description Logic cALC
Abstract: In recent years, several languages of non-classical description logics have been
introduced to model knowledge and perform inference on it. The constructive
description logic cALC deals with uncertain and dynamic knowledge and is
strictly more expressive than intuitionistic ALC. It is sub-intuitionistic and
can consistently represent situations that are incompatible with the Principle
of the Excluded Middle.
We make use of a game-theoretic dialogue-based proof technique that has its roots
in philosophy to explain reasoning in cALC and its modal-logical counterpart CKn.
This philosophical approach makes it possible to relate cALC/CKn easily with other
logics by changing the nature of the dialogues in a suitable manner. This opens a
new avenue for exploration in the proof theory of modal and description logics
which so far has been largely based on Hilbert, Gentzen and Tableaux calculi.
Paola Bruscoli, Alessio Guglielmi, Tom Gundersen and Michel Parigot. A Quasipolynomial Normalisation Procedure in Deep Inference
Abstract: Jerabek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in
quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudl´ak
about monotone sequent calculus and a correspondence between this system and cut-free deep-inference
proofs. In this work we give a direct proof of Jerabek’s result: we give a quasipolynomial-time cutelimination
procedure in propositional-logic deep inference. The main new ingredient is the use of a
computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace
only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination
procedure.
Guillaume Bonfante. Rational Bitwise Equations from a recursive point of view
Abstract: We propose to study a new form of equation. We relate
them to mutual in place recursion, which consequently provides
a new characterization of binary circuit complexity classes.
Isabel Oitavem. Rethinking FPspace with pointers
Abstract: Recursion schemes have a base function and a step function. We believe
that FPspace can be implicitly characterized using recursion with
pointers in the base function only. This is work in progress.
(joint work with Marcello Mamino)
René Gazzari. Natural Calculation
Abstract: see the PDF version