Program for Saturday, July 12th, 2014: Talk View

PROGRAM FOR SATURDAY, JULY 12TH, 2014: TALK VIEW

Days:

previous day

next day

all days

View: with abstracts session overview

9:00

9:30

10:00

10:30

11:00

11:30

12:00

12:30

13:00

13:30

14:00

14:30

15:00

15:30

16:00

16:30

17:00

17:30

18:00

18:30

19:00

08:45-08:50

LCC'14 Opening Remarks

Arnold Beckmann

08:50-09:45

Weighted Automata Theory for Complexity Analysis of Rewrite Systems

Georg Moser

09:45-10:15

Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus

Damiano Mazza

08:45-09:15

The dynamic pattern calculus as a higher-order pattern rewriting system

Vincent van Oostrom, Femke van Raamsdonk

09:15-09:45

Distilling Abstract Machines

Beniamino Accattoli

09:45-10:15

Experience with Higher Order Rewriting from the Compiler Teaching Trenches

Kristoffer Rose

09:00-09:30

Industrial-Strength Documentation for ACL2

Jared Davis, Matt Kaufmann

09:30-10:00

Enhancements to ACL2 in Versions 6.2, 6.3, and 6.4

Matt Kaufmann, J Moore

09:10-09:15

Opening Remarks

Willem Heijltjes, Kaustuv Chaudhuri, Lutz Strassburger

09:15-10:15

Simply Typed Lambda-Calculus Modulo Type Isomorphisms

Gilles Dowek

10:45-11:00

Opening

Olaf Beyersdorff

11:00-12:00

On Some Conjectures in Proof Complexity

Pavel Pudlák

10:45-11:15

Towards recursion schemata for the probablistic class PP

Reinhard Kahle, Isabel Oitavem

11:15-11:45

Closing a Gap in the Complexity of Refinement Modal Logic

Antonis Achilleos, Michael Lampis

11:45-12:15

On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic

Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere

12:15-12:45

First-Order Logic of Order and Metric has the Three-Variable Property

Timos Antonopoulos, Paul Hunter, Shahab Raza, James Worrell

10:45-11:15

Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems

Sebastiaan Joosten, Cezary Kaliszyk, Josef Urban

11:15-11:45

Polymorphic Types In ACL2

Benjamin Selfridge, Eric Smith

11:45-12:15

Data Definitions in ACL2 Sedan

Harsh Raju Chamarthi, Peter Dillinger, Panagiotis Manolios

12:15-12:45

ACL2(ml): Machine-Learning for ACL2

Jónathan Heras, Ekaterina Komendantskaya

10:45-11:15

The Higher-order Dependency Pair Framework

Cynthia Kop

11:15-11:45

Feebly not weakly

Vincent Van Oostrom

11:45-12:00

Report from the HOR 2014 Chair & Discussion

Kristoffer Rose

10:45-11:45

Completions and the Schuette method

Rosalie Iemhoff

11:45-12:15

A Correctness Criterion Free from Switchings

Marc Bagnol, Amina Doumane, Alexis Saurin

12:15-12:45

First-order Proofs Without Syntax: Summary of Work in Progress

Dominic Hughes

12:00-13:00

On Infinitary Affine Lambda-Calculi

Damiano Mazza

12:00-13:00

On Infinitary Affine Lambda-Calculi

Damiano Mazza

12:00-12:30

Size-Space Bounds and Trade-offs for CDCL Proofs

Jan Johannsen, Massimo Lauria, Jakob Nordström, Marc Vinyals

12:30-13:00

Beyond Q-Resolution and Prenex Form: A Proof System for Quantified Constraint Satisfaction

Hubie Chen

14:30-15:30

A (Biased) Survey of Space Complexity and Time-Space Trade-offs in Proof Complexity

Jakob Nordström

14:30-15:30

Search problems, proof complexity, and second-order bounded arithmetic

Sam Buss

15:30-16:00

Infinite AC0 Circuits for Parity

Benjamin Rossman

14:30-15:30

Linking ACL2 and HOL: past achievements and future prospects

Mike Gordon

14:30-15:00

Dynamical systems, attractors and well-behaved infinitary rewriting

Jakob Grue Simonsen

15:00-15:30

From the finite to the transfinite: Λμ-terms and streams.

Fanny He, Alexis Saurin

15:30-16:00

Normal Forms and Infinity

Stefan Kahrs, Connor Smith

14:30-15:30

Proof theory for ordered algebra: amalgamation and densification

Kazushige Terui

15:30-16:00

Weak topologies for Linear Logic

Marie Kerjean

14:30-15:00

A cubical representation of local states

Paul-André Melliès

15:00-15:30

Computational complexity in the lambda-calculus: what's new?

Damiano Mazza

15:30-16:00

On the parallel reduction and complexity of interaction-net systems

Stéphane Gimenez

15:30-16:00

Towards an Understanding of Polynomial Calculus: New Separations and Lower Bounds

Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, Marc Vinyals

16:30-17:00

Provably Total Search Problems in Fragments of Bounded Arithmetic Below Polynomial-time

Jean-Jose Razafindrakoto, Arnold Beckmann

17:00-17:30

Parameter-free induction in bounded arithmetic

Emil Jeřábek

17:30-18:00

Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic

Ján Pich

16:30-17:00

Descriptive Complexity and CSP

Szymon Toruńczyk

17:00-17:30

Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic

Martin Lange, Etienne Lozes

17:30-18:00

Small Dynamic Descriptive Complexity Classes

Thomas Zeume

16:30-17:00

On Vickrey's Theorem and the Use of ACL2 for Formal Reasoning in Economics

Ruben Gamboa, John Cowles

16:30-17:00

An Introduction to the Clocked Lambda Calculus

Joerg Endrullis, Dimitri Hendriks, Jan Willem Klop, Andrew Polonsky

17:00-17:30

Work in Progress: Algebraic Abstract Reduction Systems

Michele Pagani, Benoît Valiron

17:30-18:00

Turtle graphics of morphic streams

Hans Zantema

16:30-17:00

Substructural Cut Elimination

Taus Brock-Nannestad

17:00-17:30

Multiplicative Decomposition of Behaviours in Ludics

Christophe Fouqueré, Myriam Quatrini

16:30-17:00

On the Value of Variables

Beniamino Accattoli

17:00-17:30

Automated Complexity Analysis of Term Rewrite Systems

Martin Avanzini

17:30-18:00

Subrecursive Linear Dependent Types and Computational Security

Ugo Dal Lago

18:15-18:45

Proof theoretic approaches to rewriting

Thomas Powell

10:15-10:45 Coffee Break

13:00-14:30 Lunch Break

16:00-16:30 Coffee Break