VSL 2014: VIENNA SUMMER OF LOGIC 2014

PROGRAM FOR MONDAY, JULY 14TH: TALK VIEW

Days:
previous day
next day
all days

View: with abstractssession overview

LC
RTA-TLCA
CSL-LICS
SAT
ITP
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
Disclaimer | Powered by EasyChair Smart Program