VSL 2014: VIENNA SUMMER OF LOGIC 2014

PROGRAM FOR SUNDAY, JULY 13TH: TALK VIEW

Days:
previous day
next day
all days

View: with abstractssession overview

PC
WPTE
Linearity
DCM
LCC
LOLA
DTP
CLC
LSB
UNIF
ORE
IWC
GSB
QBF
FWFM
IFIP-WG16
HOL
ACL2
Isabelle
TermGraph
POS
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
08:45-09:45
Modalities and Linearity
Elaine Pimentel
09:45-10:15
The inhabitation problem for non-idempotent intersection
Simona Ronchi Della Rocca, Antonio Bucciarelli, Delia Kesner
08:45-10:15
Isabelle tutorial for beginners (part 1)
Tobias Nipkow
08:45-09:15
A formally verified proof of the Central Limit Theorem
Jeremy Avigad, Johannes Hölzl, Luke Serafin
09:15-09:45
Primitively (Co)recursive Definitions for Isabelle/HOL
Lorenz Panny, Jasmin Christian Blanchette, Dmitriy Traytel
09:45-10:15
Pattern-based Subterm Selection In Isabelle
Lars Noschinski, Christoph Traut
08:45-09:30
A Unified Proof System for QBF Preprocessing
Marijn Heule
09:30-10:15
On Instantiation-Based Calculi for QBF
Mikolas Janota
08:45-09:00
Welcome
Organisers
09:00-09:30
Using HOL4 to Formalize Physical Systems
Umair Siddique, Sofiene Tahar
09:30-10:00
Modernising HOL's documentation
Magnus O. Myreen
08:45-09:15
Decision Procedures for Proving Inductive Theorems without Induction
Takahito Aoto, Sorin Stratulat
09:15-10:00
Discussion on the International School on Rewriting (ISR)
Aart Middeldorp, Mauricio Ayala Rincón, Alfons Geser
08:45-09:00 Welcome
09:00-09:15
Opening
Manfred Schmidt-Schauß
09:15-10:15
HERMIT: An Equational Reasoning Model to Implementation Rewrite System for Haskell
Andrew Gill
09:00-09:05
Welcome
Organizers
09:05-09:50
Semantics and Proof Theory in Team Play: the case of Paraconsistent Logics
Anna Zamansky
09:50-10:15
On the Construction of Analytic Sequent Calculi for Sub-classical Logics
Ori Lahav, Yoni Zohar
09:00-09:15
Opening
Temur Kutsia, Christophe Ringeissen
09:15-10:15
Extensible Symbolic System Analysis
Jose Meseguer
09:00-09:15 Opening
09:00-09:30
Formal Verification of Medina's Sequence of Polynomials for Approximating Arctangent
Ruben Gamboa, John Cowles
09:30-10:00
Equivalence of the Traditional and Non-Standard Definitions of Concepts from Real Analysis
John Cowles, Ruben Gamboa
09:00-09:15
ImmermanFest Opening Remarks
Kousha Etessami
09:15-10:15
27 and still counting: Iterated product, inductive counting, and the structure of P
Eric Allender
09:00-10:00
FRP, LTL and GUIs
Alan Jeffrey
09:00-09:15
Fun With Formal Methods 2014: Opening Remarks
Nikolay Shilov
09:15-10:15
Algebraic description of restricted programming and elements of its logics
Nikolay Nepejvoda
09:00-10:00
TBC
Alexandre Miquel
10:00-10:20
Extensional Models of Typed Lambda-mu Calculus
Koji Nakazawa
09:15-10:15
Numeral Systems in the Lambda Calculus
Ian Mackie
09:15-10:15
Numeral Systems in the Lambda Calculus
Ian Mackie
09:15-09:45
Dolius: A Distributed Parallel SAT Solving Framework
Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Cédric Piette
09:45-10:15
Validating Unsatisfiability Results of Clause Sharing Parallel SAT Solvers
Marijn Heule, Norbert Manthey, Tobias Philipp
09:15-09:45
Quasipolynomial Size Frege Proofs of Frankl's Theorem on the Trace of Finite Sets
James Aisenberg, Maria Bonet, Sam Buss
09:45-10:15
n^O(log log n) size monotone proofs of the weak pigeonhole principle
Anupam Das
09:15-10:15
An algebraic approach for inferring and using symmetries in rule-based models
Jerome Feret
09:15-10:15
De haut en bas: relating high-level and low-level abstractions
Nick Benton
09:25-10:15
On the Formalization of Lambda-Calculus Confluence and Residuals
Beniamino Accattoli
10:45-11:45
Some Reflections on Definability and Complexity
Phokion Kolaitis
11:45-12:45
Crane Beach Revisited
Nicole Schweikardt
10:45-11:15
Undecidability of Multiplicative Subexponential Logic
Kaustuv Chaudhuri
11:15-11:45
Superstructural Reversible Logic
Zachary Sparks, Amr Sabry
11:45-12:15
A Linear/Producer/Consumer model of Classical Linear Logic
Jennifer Paykin, Steve Zdancewic
12:15-12:45
Cut Elimination in Multifocused Linear Logic
Taus Brock-Nannestad, Nicolas Guenot
10:45-11:15
Verifying Optimizations for Concurrent Programs
William Mansky, Elsa Gunter
11:15-11:45
Inverse Unfold Problem and Its Heuristic Solving
Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, Naoki Nishida
11:45-12:00
Short break
Break
12:00-12:30
Structural Rewriting in the Pi-Calculus
David Sabel
12:30-13:00
Attractor Equivalence: An Observational Semantics for Reaction Networks
Guillaume Madelaine, Cedric Lhoussaine, Joachim Niehren
10:45-12:45
Isabelle tutorial for beginners (part 2)
Tobias Nipkow
10:45-10:55
The CoCon Experiment
Andrei Popescu, Peter Lammich
10:55-11:20
The CAVA Automata Library
Peter Lammich
11:20-11:45
From Types to Sets in Isabelle/HOL
Ondřej Kunčar, Andrei Popescu
11:45-12:15
Towards abstract and executable multivariate polynomials in Isabelle
Florian Haftmann, Andreas Lochbihler, Wolfgang Schreiner
12:15-12:45
Tutorial: Isabelle/jEdit for seasoned Isabelle users
Makarius Wenzel
10:45-11:15
Needed Computations Shortcutting Needed Steps
Sergio Antoy, Jacob Johannsen, Steven Libby
11:15-11:45
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
Naohi Eguchi
11:45-12:15
Nested Term Graphs
Clemens Grabmayer, Vincent van Oostrom
10:45-11:10
Comparing Sequent Calculi via Hilbert-style Axioms
Björn Lellmann
11:10-11:35
Sequent Systems for Classical Modal Logics
Paolo Maffezioli, David Gilbert
11:35-12:00
Lyndon Interpolation for the Modal Mu-Calculus
Daniyar Shamkanov
12:00-12:25
On cuts and cut-elimination in modal fixed point logics
Thomas Studer
12:25-12:50
Display-type calculi and their cut elimination metatheorem
G. Greco, S. Frittella, A. Kurz, A. Palmigiano, V. Sikimić
10:45-11:15
On the Relation between Resolution Calculi for QBFs and First-order Formulas
Uwe Egly
11:15-11:45
Resolution Paths and Term Resolution
Friedrich Slivovsky, Stefan Szeider
11:45-12:15
Efficient Extraction of QBF (Counter)models from Long-Distance Resolution Proofs
Valeriy Balabanov, Jie-Hong Roland Jiang, Mikoláš Janota, Magdalena Widl
12:15-12:45
Dependency Quantified Boolean Formulas - Challenges, Applications, First Lines of Attack
Christoph Scholl
10:45-11:15
Writing proof automation for HOL4
Magnus O. Myreen
11:15-12:45
Hack Session 1
Everyone
10:45-11:15
Certification of Confluence Proofs using CeTA
Julian Nagele, René Thiemann
11:15-11:45
Confluence and Critical-Pair-Closing Systems
Michio Oyamaguchi, Nao Hirokawa
10:45-11:00 ORE Opening
10:45-11:15
Unification Modulo Common List Functions
Peter Hibbs, Paliath Narendran, Shweta Mehto
11:15-11:45
Matching with respect to general concept inclusions in the Description Logic EL
Franz Baader, Barbara Morawska
11:45-12:15
Unification in the normal modal logic Alt1
Philippe Balbiani, Tinko Tinchev
12:15-12:35
On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
S. Erbatur, D. Kapur, A.M. Marshall, C. Meadows, P. Narendran, C. Ringeissen
12:35-12:55
Hierarchical Combination of Matching Algorithms (Extended Abstract)
S. Erbatur, D. Kapur, A.M. Marshall, P. Narendran, C. Ringeissen
10:45-11:15
Post Mortem Analysis of SAT Solver Proofs
Laurent Simon
11:15-11:45
Formula partitioning revisited
Zoltan Mann, Pal Papp
11:45-12:15
New CNF Features and Formula Classification
Norbert Manthey, Enrique Alfonso
12:15-12:45
Typical-case complexity and the SAT competitions
Zoltan Mann
10:45-11:45
Weak Pigeonhole Principles, Circuits for Approximate Counting, and Bounded-Depth Proofs
Albert Atserias
10:45-11:30
Rewriting, Proofs and Transition Systems
Gilles Dowek, Ying Jiang
11:30-12:00
Semantically-Guided Goal-Sensitive Theorem Proving
Maria Paola Bonacina, David Plaisted
12:00-12:30
Impacts of the Digital Revolution on two Main Activities of Scientists: Teaching and Publishing
Claude Kirchner
12:30-13:00
Discussion on Massive Open Online Courses and Overlay Journals
Claude Kirchner
10:45-11:30
Using answer set programming to integrate large-scale heterogeneous information about the response of a biological
Anne Siegel
11:30-12:15
Attractor equivalence: An observational semantics for reaction networks
Cedric Lhoussaine
12:15-12:55
A Logical Framework for Systems Biology
Elisabetta de Maria, Joelle Despeyroux, Amy Felty
10:45-11:15
Modeling Algorithms in SystemC and ACL2
David Russinoff, John O'Leary
11:15-11:45
Development of a Translator from LLVM to ACL2
David Hardin, Jennifer Davis, David Greve, Jedidiah McClurg
11:45-12:15
An ACL2 Mechanization of an Axiomatic Framework for Weak Memory
Benjamin Selfridge
12:15-12:45
Using ACL2 to Verify Loop Pipelining in Behavioral Synthesis
Disha Puri, Sandip Ray, Kecheng Hao, Fei Xie
10:45-11:15
Terminal semantics for codata types in intensional Martin-Löf type theory
Benedikt Ahrens, Régis Spadotti
11:15-11:45
A Unifying Framework for Primitive Ontological Relations in Dependent Type Theory
Richard Dapoigny, Patrick Barlatier
11:45-12:15
Domain Specific Languages of Mathematics
Cezar Ionescu, Patrik Jansson
12:15-12:45
Relational ornaments
Hsiang-Shang Ko, Jeremy Gibbons
10:45-11:15
A Simple Parallel Implementation of Interaction Nets in Haskell
Wolfram Kahl
11:15-11:45
Some observations for the parallel implementation of interaction nets
Ian Mackie, Shinya Sato
10:45-11:15
Abstract Self Modifying Machines
Hubert Godfroy, Jean-Yves Marion
11:15-11:45
Programming and Verifying with Effect Handling and Iteration
Sergey Goncharov, Lutz Schröder, Christoph Rauch
11:45-12:15
Tensorial logic with algebraic effects
Paul-André Melliès
12:15-12:45
Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of
Koko Muroya, Toshiki Kataoka, Ichiro Hasuo, Naohiko Hoshino
10:50-11:10
A Translation of Intersection and Union Types for the lambda-mu Calculus
Kentaro Kikuchi, Takafumi Sakurai
11:10-11:30
Dualized Type Theory
Harley Eades Iii, Aaron Stump, Ryan McCleeary
11:30-12:00
A proof-theoretic view on scheduling in concurrency
Emmanuel Beffara
12:00-12:30
A type system for Continuation Calculus
Herman Geuvers, Wouter Geraedts, Bram Geron, Judith van Stegeren
12:30-13:00
Confluence for classical logic through the distinction between values and computations
José Espírito Santo, Ralph Matthes, Koji Nakazawa, Luís Pinto
11:00-11:20
TROvE: a Graphical Tool to Evaluate OWL Reasoners
Jean-Rémi Bourguet, Luca Pulina
11:20-11:40
Using OpenStreetMap Data to Create Benchmarks for Description Logic Reasoners
Thomas Eiter, Patrik Schneider, Mantas Simkus, Guohui Xiao
11:40-12:00
A Scalable Benchmark for OBDA Systems: Preliminary Report
Diego Calvanese, Davide Lanti, Martin Rezk, Mindaugas Slusnys, Guohui Xiao
12:00-12:20
Evaluating OWL 2 Reasoners in the Context Of Checking Entity-Relationship Diagrams During Software
Alexander Kropotin
12:20-12:40
Just: a Tool for Computing Justifications w.r.t. ELH Ontologies
Michel Ludwig
12:40-13:00
Android Went Semantic: Time for Evaluation
Carlos Bobed, Fernando Bobillo, Roberto Yus, Guillermo Esteban, Eduardo Mena
11:00-11:30
Chekofv: Crowd-sourced Formal Verification
Heather Logas, Florent Kirchner, John Murray, Martin Schäf, Jim Whitehead
11:30-12:00
Using Esoteric Language for Teaching Formal Semantics
Nikolay Shilov
12:00-12:30
Introducing Formal Verification with Lego
Lawrence et.al
12:30-13:00
Explaining the decompositionality of MSO using applications to combinatorics
Tomer Kotek
12:00-12:30
Critical Pairs in Network Rewriting
Lars Hellström
12:30-13:00
On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent
Naoki Nishida, Makishi Yanagisawa, Karl Gmeiner
12:00-12:30
Total Space in Resolution
Ilario Bonacina, Nicola Galesi, Neil Thapen
12:30-13:00
From Small Space to Small Width in Resolution
Yuval Filmus, Massimo Lauria, Mladen Miksa, Jakob Nordström, Marc Vinyals
12:00-13:00
Quantitative semantics for higher-order probabilistic and quantum computation
Michele Pagani
14:00-15:00
On the power of fixed-point logic with counting
Anuj Dawar
15:00-16:00
Reasoning about transitive closure in Immerman's style
Mooly Sagiv
14:30-15:30
Continuations, closed reduction and process networks
Ian Mackie
15:30-16:00
Type Classes for Lightweight Substructural Types
Edward Gan, Jesse A. Tov, Greg Morrisett
14:30-15:00
On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using
Naoki Nishida, Makishi Yanagisawa, Karl Gmeiner
15:00-15:30
Contextual Equivalences in Call-by-Need and Call-By-Name Polymorphically Typed Calculi (Preliminary
Manfred Schmidt-Schauss, David Sabel
15:30-16:00
Verifying the Correctness of Tupling Transformations based on Conditional Rewriting
Yuki Chiba
14:30-15:00
Proving Gödel’s Incompleteness Theorems
Lawrence Paulson
15:00-15:30
Isabelle/jEdit NEWS
Makarius Wenzel
15:30-16:00
Programming TLS in Isabelle/HOL
Andreas Lochbihler, Marc Züst
14:30-15:30
An Introduction to Higher-Dimensional Rewriting Theory
Samuel Mimram
14:30-15:30
An Introduction to Higher-Dimensional Rewriting Theory
Samuel Mimram
14:30-15:15
Cyclic proof for quantitative logics
Alex Simpson
15:15-15:40
Modular Systems for Intuitionistic Modal Logics in Nested Sequents
Sonia Marin, Lutz Straßburger
15:40-16:05
An Intuitionisticaly based Description Logic
Alexandre Rademaker, Hermann Haeusler
14:30-15:00
Incremental QBF Reasoning for the Verification of Partial Designs
Paolo Marin, Christian Miller, Bernd Becker
15:00-15:30
Reactive Synthesis using (Incremental) QBF Solving
Robert Koenighofer
15:30-16:00
Conformant Planning as a Case Study of Incremental QBF Solving
Martin Kronegger, Andreas Pfandler, Florian Lonsing, Uwe Egly
14:30-15:00
HOL4 Hidden Features
Anthony Fox
15:00-15:30
New Styles of Proof
Ramana Kumar
15:30-16:00
Hack Session 2
Everyone
14:30-14:50
Exploring Reasoning with the DMOP Ontology
C. Maria Keet, Claudia D'Amato, Zubeida Khan, Agnieszka Lawrynowicz
14:50-15:10
An update on Genomic CDS, a complex ontology for pharmacogenomics and clinical decision support
José Antonio Minarro-Giménez, Matthias Samwald
15:10-15:30
A Family History Knowledge Base in OWL 2
Robert Stevens, Nicolas Matentzoglu, Uli Sattler
14:30-15:30
On the Limits of Second-Order Unification
Jordi Levy
15:30-16:00
From Admissibility to a New Hierarchy of Unification Types
Leonardo Manuel Cabrer, George Mectalfe
14:30-15:30
Lingeling Essentials, A Tutorial on Design and Implementation Aspects of the the SAT Solver
Armin Biere
14:30-15:30
Are matrix identities hard instances for strong proof systems?
Iddo Tzameret
14:30-15:15
Basic Normalization
Nao Hirokawa, Aart Middeldorp, Georg Moser
15:15-16:00
Rhythm Tree Rewriting
Florent Jacquemard, Jean Bresson, Pierre Donat-Bouillud
14:30-15:15
TBA
Alessandra Carbone
15:15-16:00
Model Checking the Evolution of Gene Regulatory Networks
Thomas Henzinger
14:30-15:30
Machine-code verification: experience of tackling medium-sized case studies using 'decompilation into
Magnus Myreen
14:30-15:00
An Embedded Hardware Description Language using Dependent Types
João Paulo Pizani Flor, Wouter Swierstra
15:00-15:30
Type-Directed Editing for Dependently-Typed Programs.
Edward Amsden, Ryan Newton, Jeremy Siek
15:30-16:00
Tool Demonstration: An IDE for Programming and Proving in Idris
Hannes Mehnert, David Raymond Christiansen
14:30-15:00
Towards the Application of Formal Methods in Process Engineering
Sidi Mohamed Beillahi, Umair Siddique, Sofiene Tahar
15:00-15:30
An Example Demonstrating the Requirement of Fully Formal Verification Method
Pratima K. Shah
14:30-15:00
Cellular Automata are Generic
Nachum Dershowitz, Evgenia Falkovich
15:00-15:30
Quantum Circuits for the Unitary Permutation Problem
Stefano Facchini, Simon Perdrix
15:30-16:00
Propositional Logics Complexity and the sub-formula Property
Edward Hermann Haeusler
14:30-15:00
Infinitary Classical Logic: Recursive Equations and Interactive Semantics
Michele Basaldella
15:00-15:20
Separable Sequent Calculus for First-order Classical Logic (Work in Progress)
Dominic Hughes
15:20-15:40
Cut-Elimination in Schematic Proofs and Herbrand Sequents
David Cerna, Alexander Leitsch
15:40-16:00
Stratified Nested Linear Logic
Matthieu Perrinel
15:00-16:00
On Machines, Virtual Memory and Successful System Verification
Rafal Kolanski
15:30-16:00 ORE Competition Session
15:30-16:00
Confluence of linear rewriting and homology of algebras
Yves Guiraud, Eric Hoffbeck, Philippe Malbos
15:30-16:00
Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers
Norbert Manthey, Peter Steinke, Steffen Hölldobler, Tobias Philipp
15:30-16:00 Panel Discussion
15:30-16:00
Lower bounds for splittings by linear combinations
Dmitry Itsykson, Dmitry Sokolov
15:30-16:00
Injectivity of Relational Semantics for (Connected) MELL Proof-Nets via Taylor Expansion
Giulio Guerrieri, Luc Pellissier, Lorenzo Tortora De Falco
16:30-17:30
The Variable Hierarchy on Ordered Graphs
Benjamin Rossman
17:30-17:45
Closing Remarks
Neil Immerman
16:30-17:00
Ludics without Designs I: Triads
Michele Basaldella
17:00-17:30
Wave-Style Token Machines and Quantum Lambda Calculi
Ugo Dal Lago, Margherita Zorzi
17:30-18:00
Geometry of Resource Interaction – A Minimalist Approach
Marco Solieri
18:00-18:30
A new point of view on the Taylor expansion of proof-nets and uniformity
Giulio Guerrieri, Lorenzo Tortora De Falco
16:30-17:00
Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems
Karl Gmeiner, Naoki Nishida
17:00-17:30
A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems
Georg Moser, Michael Schaper
17:30-17:45
Closing
Manfred Schmidt-Schauß
16:30-17:00
Using Isabelle/HOL to Develop and Maintain Separation Invariants for an Operating System (Extended
Blasum et.al
17:00-17:20
A Simpl Shortest Path Checker Verification
Christine Rizkallah
17:20-17:40
Towards Structured Proofs for Program Verification (Ongoing Work)
Lars Noschinski
17:40-18:00
Amortized Complexity Verified
Tobias Nipkow
16:30-17:00
An Implementation Model for Interaction Nets
Ian Mackie, Shinya Sato
17:00-17:30
Fixed Point Theory for Consistent Rewriting in Logic of Action with Reverse
Susumu Yamasaki
16:30-16:55
Link formulas in implication fragments of substructural logics
Tomasz Kowalski
16:55-17:20
A proof theoretic approach to standard completeness
Paolo Baldi
17:20-17:45
On Affine Logic and Łukasiewicz Logic
Rob Arthan, Paulo Oliva
17:45-18:10
Simpler Proof Net Quantifiers: Unification Nets (Work in Progress)
Dominic Hughes
16:30-17:00
Synthesis of distributed systems using QBF
Adrià Gascón
17:00-18:00
The QBF Gallery 2014
Martina Seidl, Charles Jordan
16:30-17:00
Discussion Session
Everyone
17:00-18:30
Hack Session 3
Everyone
16:30-17:00
Normalization Equivalence of Rewrite Systems
Nao Hirokawa, Aart Middeldorp, Christian Sternagel
17:00-17:30
Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract)
Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa
17:30-18:15
Confluence Competition
Takahito Aoto, Nao Hirokawa, Harald Zankl
16:30-16:50
Mini-ME 2.0: powering the Semantic Web of Things
M. Ruta, F. Scioscia, G. Loseto, F. Gramegna, S. Ieva, E. Di Sciascio
16:50-17:10
Incremental and Persistent Reasoning in FaCT++
Dmitry Tsarkov
16:30-17:00
Constraint Manipulation in SGGS
Maria Paola Bonacina, David Plaisted
17:00-17:30
Two-sided unification is NP-complete
Tatyana Novikova, Vladimir Zakharov
17:30-18:00
Nominal Anti-Unification
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret
16:30-17:00
iDQ: Instantiation-Based DQBF Solving
Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith
17:00-17:30
Instance-based Selection of CSP Solvers using Short Training
Mirko Stojadinovic, Filip Maric
17:30-18:00
Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle
T. Soh, D. Le Berre, S. Roussel, M. Banbara, N. Tamura
16:30-17:00
Narrow Proofs May Be Maximally Long
Albert Atserias, Massimo Lauria, Jakob Nordström
17:00-17:30
Parity games and propositional proofs
Neil Thapen, Arnold Beckmann, Pavel Pudlák
16:30-17:00
Discussion on the Future of RTA (+ TLCA)
Georg Moser
17:00-17:30
Discussion on the Open Problems List in Rewriting
Nachum Dershowitz, Hans Zantema
17:30-18:00
Business Meeting
Jürgen Giesl
16:30-17:30
The role of domain specific languages in simulation studies - Analyzing the impact of membrane dynamics on the Wnt signaling
Adelinde Uhrmacher
16:30-18:00 Panel Discussion about low-level code verification
16:30-17:00
Scrapping Your Dependently-Typed Boilerplate is Hard
Ahmad Salim Al-Sibahi
17:00-17:30
On a style of presentation of type systems
Alvaro Tasistro
17:30-18:00
Sequential decision problems, dependent types and generic solutions
Nicola Botta, Cezar Ionescu, Patrik Jansson, Edwin Brady
16:30-17:00
Probabilistic Types and Function Overloading
Alessandra Di Pierro, Margherita Zorzi
17:00-17:30
Differential privacy at work: Verification of approximate probabilistic programs and models for choosing
Marco Gaboardi, Justin Hsu
17:30-18:00
Interactive Particle Systems and Random Walks on Hypergraphs
Gabriel Istrate, Cosmin Bonchis, Mircea Marin
16:30-17:00
A Cross-Language Framework for Verifying Compiler Optimizations
William Mansky, Elsa Gunter
17:00-17:30
Call-by-Value in a Basic Logic for Interaction
Ulrich Schöpp
16:30-17:00
A sheaf model of the algebraic closure
Bassel Mannaa, Thierry Coquand
17:00-17:20
A "Game Semantical" Intuitionistic Realizability Validating Markov's Principle
Federico Aschieri, Margherita Zorzi
17:20-17:40
Relative Computability and Uniform Continuity of Non-Extensional (aka Multivalued) 'Functions'
Arno Pauly, Martin Ziegler
17:40-18:00
Negative Translations and Heyting Algebra Expansions
Tadeusz Litak
17:10-17:15 ORE closing
18:00-18:30
A Categorical Perspective on Pattern Unification (Extended Abstract)
Andrea Vezzosi, Andreas Abel
18:30-19:00
Towards a better-behaved unification algorithm for Coq
Beta Ziliani, Matthieu Sozeau
18:15-21:00 Workshop dinner in honor of Immerman
10:15-10:45 Coffee Break
13:00-14:30 Lunch Break
16:00-16:30 Coffee Break
Disclaimer | Powered by EasyChair Smart Program