VSL 2014: VIENNA SUMMER OF LOGIC 2014

PROGRAM FOR SATURDAY, JULY 12TH: TALK VIEW

Days:
previous day
next day
all days

View: with abstractssession overview

PC
WIR
LCC
HOR
SD
ACL2
2FC
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
Disclaimer | Powered by EasyChair Smart Program