Program for Monday, July 14th, 2014: Talk View

PROGRAM FOR MONDAY, JULY 14TH, 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

19:30

20:00

20:30

21:00

21:30

10:45-12:45

Computer-checked mathematics: a formal proof of the Odd Order theorem

Assia Mahboubi

10:45-11:15

A quest for algorithmically random infinite structures

Bakh Khoussainov

11:15-11:45

On the Total Variation Distance of Labelled Markov Chains

Taolue Chen, Stefan Kiefer

11:45-12:15

A domain-theoretic approach to Brownian motion and general continuous stochastic processes

Paul Bilokon, Abbas Edalat

12:15-12:45

On the Computing Power of +, −, and ×

Marcello Mamino

10:45-11:15

Towards a Formally Verified Proof Assistant

Abhishek Anand, Vincent Rahli

11:15-11:45

The reflective Milawa theorem prover is sound (down to the machine code that runs it)

Magnus O. Myreen, Jared Davis

11:45-12:15

HOL with Definitions: Semantics, Soundness, and a Verified Implementation

Ramana Kumar, Rob Arthan, Magnus O. Myreen, Scott Owens

12:15-12:45

Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete

J Strother Moore

12:45-13:00

Rough Diamond: An Extension of Equivalence-based Rewriting

Matt Kaufmann, J Moore

10:45-11:15

Implicational Relevance Logic is 2-ExpTime-Complete

Sylvain Schmitz

11:15-11:45

An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting

Daniel de Carvalho, Jakob Grue Simonsen

11:45-12:15

Unification and Logarithmic Space

Marc Bagnol, Clément Aubert

12:15-12:45

Automated Complexity Analysis Based on Context-Sensitive Rewriting

Nao Hirokawa, Georg Moser

12:45-13:00

Automatic Evaluation of Context-Free Grammars (System Description)

Carles Creus, Guillem Godoy

10:45-11:15

Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction

Takayuki Sakai, Kazuhisa Seto, Suguru Tamaki

11:15-11:45

Solving MaxSAT and #SAT on structured CNF formulas

Jan Arne Telle, Sigve Hortemo Sæther, Martin Vatshelle

11:45-12:05

Cores in Core based MaxSat Algorithms: an Analysis

Fahiem Bacchus, Nina Narodytska

11:00-12:00

Tutorial on Stategic and Extensive Games 1

Krzysztof Apt

12:00-13:00

Applications of admissible computability

Noam Greenberg

12:10-12:40

On Computing Preferred MUSes and MCSes

Alessandro Previti, Joao Marques-Silva

12:40-13:00

MUS Extraction using Clausal Proofs

Anton Belov, Marijn Heule, Joao Marques-Silva

14:30-16:00

Understanding Biology through Logic

Jasmin Fisher

14:30-15:00

From Operational Models to Information Theory - Side-Channels in pGCL with Isabelle

David Cock

15:00-16:00

Invited talk: Microcode Verification - Another Piece of the Microprocessor Verification Puzzle

Anna Slobodova, Jared Davis, Sol Swords

14:30-15:30

Process types as a descriptive tool for distributed protocols

Nobuko Yoshida

15:30-16:00

Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB

Manfred Schmidt-Schauss, David Sabel

14:30-15:00

Fixed-parameter tractable reductions to SAT

Ronald de Haan, Stefan Szeider

15:00-15:30

On Reducing Maximum Independent Set to Minimum Satisfiability

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

15:30-15:50

Conditional Lower Bounds for Failed Literals and Related Techniques

Matti Järvisalo, Janne H. Korhonen

14:30-15:15

The DNA of logic and games.

Johan Van Benthem

15:15-16:00

Dependence and independence - a logical approach

Jouko Väänänen

14:30-15:15

Pregeometries and definable groups

Pantelis Eleftheriou

15:15-16:00

Quasiminimal structures and excellence

Meeri Kesala

14:30-15:15

Uniform and non-uniform reducibilities of algebraic structures

Iskander Kalimullin

15:15-16:00

Randomness in the Weihrauch degrees

Rupert Hölzl

14:30-15:15

Inductive Proofs & the Knowledge They Represent

Michael Detlefsen

15:15-16:00

Decidable languages for knowledge representation and inductive definitions: From Datalog to

Georg Gottlob

14:30-15:15

Inductive Proofs & the Knowledge They Represent

Michael Detlefsen

15:15-16:00

Decidable languages for knowledge representation and inductive definitions: From Datalog to

Georg Gottlob

16:30-17:00

Turing Machines with Atoms, Constraint Satisfaction Problems, and Descriptive Complexity

Bartek Klin, Sławomir Lasota, Joanna Ochremiak, Szymon Toruńczyk

17:00-17:30

Beta Reduction is Invariant, Indeed

Beniamino Accattoli, Ugo Dal Lago

17:30-18:00

On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems

Anupam Das

18:00-18:30

Faster decision of first-order graph properties

Ryan Williams

16:30-17:00

Logic for Communicating Automata with Parameterized Topology

Benedikt Bollig

17:00-17:30

Equilibria of Concurrent Games on Event Structures

Julian Gutierrez, Michael Wooldridge

17:30-18:00

Compositional Verification of Termination-Preserving Refinement of Concurrent Programs

Hongjin Liang, Xinyu Feng, Zhong Shao

18:00-18:30

Symmetry in Concurrent Games

Simon Castellan, Pierre Clairambault, Glynn Winskel

16:30-17:00

Truly Modular (Co)datatypes for Isabelle/HOL

J.C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu, D. Traytel

17:00-17:30

Recursive Functions on Codatatypes via Domains and Topologies

Andreas Lochbihler, Johannes Hölzl

17:30-18:00

Experience Implementing a Performant Category-Theory Library in Coq

Jason Gross, Adam Chlipala, David Spivak

16:30-17:00

A Coinductive Confluence Proof for Infinitary Lambda-Calculus.

Łukasz Czajka

17:00-17:30

Confluence by Critical Pair Analysis

Jiaxiang Liu, Nachum Dershowitz, Jean-Pierre Jouannaud

17:30-18:00

Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams

Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida

18:00-18:15

Conditional Confluence (System Description)

Thomas Sternagel, Aart Middeldorp

16:30-16:50

MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing

Charles Jordan, Lukasz Kaiser, Florian Lonsing, Martina Seidl

16:50-17:10

DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs

Nathan Wetzler, Marijn Heule, Warren Hunt

17:10-17:30

Automatic Evaluation of Reductions between NP-complete Problems

Carles Creus, Pau Fernández, Guillem Godoy

17:30-17:50

Open-WBO: a Modular MaxSAT Solver

Ruben Martins, Vasco Manquinho, Ines Lynce

16:30-16:50

Natural deduction for intuitionistic differential linear logic

Mattia Petrolo, Giulio Guerrieri

16:50-17:10

An outline of intuitionistic epistemic logic

Sergei Artemov, Tudor Protopopescu

17:10-17:30

Some properties related to the existence property in intermediate predicate logics

Nobu-Yuki Suzuki

17:30-17:50

On Hallden complete modal logics determined by homogeneous frames

Zofia Kostrzycka

17:50-18:10

A universal diagonal schema by fixed-points and Yablo’s paradox

Ahmad Karimi, Saeed Salehi

18:10-18:30

Canonical extensions and prime filter completions of poset expansions.

Wilmari Morton, Clint van Alten

16:30-16:50

On the compactness theorem in many valued logics

Hovhannes Bolibekyan

16:50-17:10

Formalizing vagueness as a doxastic, relational concept

Thomas Benda

17:10-17:30

Two Formalisms for a Logic of Generalized Truth Values

Oleg Grigoriev

17:30-17:50

Characterising Logics through their Admissible Rules

Jeroen Goudsmit

17:50-18:10

Models for the probabilistic sequent calculus

Marija Boricic

18:10-18:30

Display-type calculi for non classical logics

Sabine Frittella

16:30-16:50

Complexity bounds for Multiagent Justification Logic

Antonis Achilleos

16:50-17:10

The relation between the graphs structures and proof complexity of corresponding Tseitin graph

Armen Mnatsakanyan

17:10-17:30

The algorithmic complexity of decomposability in fragments of first-order logic

Denis Ponomaryov

17:30-17:50

Type equations and second order logic

Paolo Pistone

17:50-18:10

An intuitive semantics for {Full Intuitionistic Linear Logic}

Valeria de Paiva, Luiz Carlos Pereira

18:10-18:30

Argumentation Logic

Antonis Kakas, Francesca Toni, Paolo Mancarella

16:30-16:50

On the existential interpretability of structures

Andrey Morozov, Aizhan Satekbaeva, Jamalbek Tussupov

16:50-17:10

The isomorphism problem for computable projective planes

Nurlan Kogabaev

17:10-17:30

Coding graphs into fields

R. Miller, J. Park, B. Poonen, H. Schoutens, A. Shlapentokh

17:30-17:50

Uniformization in the hereditarily finite list superstructure over the real exponential field

Svetlana Aleksandrova

17:50-18:10

Dynamic logic on approximation spaces

Alexey Stukachev

18:10-18:30

On limitwise monotonic reducibility of Σ^0_2-sets.

Damir Zainetdinov, Iskander Kalimullin

16:30-16:50

Relativized universal numberings

Serikzhan Badaev, Sergey Goncharov

16:50-17:10

Ideals without minimal numberings in the Rogers semilattice

Assylbek Issakhov

17:10-17:30

Computable numberings in Analytical Hierarchy

Marina Dorzhieva

17:30-17:50

Definability of 0' in the structure of $\omega$-enumeration degrees

Andrey Sariev

17:50-18:10

Embedding the omega-enumeration degrees into the Muchnik degrees generated by spectra of structures

Stefan Vatev

18:10-18:30

Limitwise monotonic sets of reals

Marat Faizrahmanov, Iskander Kalimullin

16:30-16:50

An Intuitionistic Interpretation of Classical Implication

Branislav Boricic, Mirjana Ilic

16:50-17:10

Predicate Glivenko theorems and substructural aspects of negative translations

Hadi Farahani, Hiroakira Ono

17:10-17:30

Adding a Conditional to Kripke's Theory of Truth

Lorenzo Rossi

17:30-17:50

Constructive completeness and Joyal's theorem

Henrik Forssell

17:50-18:10

Algorithmic-algebraic canonicity for mu-calculi

Willem Conradie, Andrew Craig

18:10-18:30

Proof-Theoretic Analysis of Brouwer's Argument of the Bar Induction

Ryota Akiyoshi

16:30-16:50

On Explicit-Implicit Reflection Principles.

Elena Nogina

16:50-17:10

Ordinal Notations and Fundamental Sequences in Caucal Hierarchy

Fedor Pakhomov

17:10-17:30

The maximal order type of the trees with the gap-embeddability relation

Jeroen Van der Meeren

17:30-17:50

Computational reverse mathematics and foundational analysis

Benedict Eastaugh

17:50-18:10

Semantic completeness of first order theories in constructive reverse mathematics

Christian Espindola

18:10-18:30

Reverse Mathematics, more explicitly

Sam Sanders

16:30-16:50

A computability approach to three hierarchies

Linda Brown Westrick

16:50-17:10

A generalization of Solovay's Sigma-construction with application to intermediate models

Vladimir Kanovei

17:10-17:30

A new lower bound for the length of the hierarchy of norms

Alexander Block

17:30-17:50

Unraveling $\Sigma^0_\alpha(\Pi^1_1)$-Determinacy

Sherwood Hachtman

17:50-18:10

Determinacy of Refinements to the Difference Hierarchy of Co-analytic sets

Chris Le Sueur

18:10-18:30

On proof complexities of strong equal modal tautologies.

Anahit Chubaryan, Armen Mnatsakanyan, Hakob Nalbandyan

16:30-16:50

Reducts of simple (non-collapsed) Fraisse-Hrushovski constructions

Omer Mermelstein

16:50-17:10

On Jonsson sets and some their properties.

Aibat Yeshkeyev

17:10-17:30

Ultraproduct construction of representative utility functions with infinite-dimensional domain

Geghard Bedrosian, Frederik Herzberg

17:30-17:50

An axiomatic approach to modelling of orders of magnitude

Bruno Dinis, Imme Van den Berg

17:50-18:10

Elementary numerosities and measures.

Emanuele Bottazzi

16:30-16:50

Differential Galois theory in the class of formally real fields.

Quentin Brouette, Françoise Point

16:50-17:10

Around n-dependent fields

Nadja Hempel

17:10-17:30

Some remarks on $\aleph_0$-categorical weakly circularly minimal structures

Beibut Kulpeshov

17:30-17:50

Uniqueness of limit models in metric abstract elementary classes under categoricity and some consequences in domination and orthogonality of Galois

Pedro Zambrano, Andres Villaveces

17:50-18:10

Amalgamation, characterizing cardinals and locally finite Abstract Elementary Classes

Martin Koerwien, John T. Baldwin, Michael C. Laskowski

18:10-18:30

Computing the number of types of infinite tuples

Will Boney

18:00-18:30 ITP business meeting

08:45-08:50

Welcome Address by the Rector

Sabine Seidler

08:50-08:55

Welcome Address by the Organizers

Matthias Baaz, Thomas Eiter, Helmut Veith

08:55-09:15

VSL Opening

Dana Scott

09:15-10:15

VSL Keynote Talk: Computational Ideas and the Theory of Evolution

Christos Papadimitriou

10:15-10:45 Coffee Break

13:00-14:30 Lunch Break

16:00-16:30 Coffee Break

20:00-21:30 VSL Opening Reception