Program for Saturday, July 7th: Talk View

PROGRAM FOR SATURDAY, JULY 7TH: 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

22:00

09:00-10:00

Sheaf models of classical logic extended by independence relations

Alex Simpson

10:00-10:30

Towards a Dualized Sequent Calculus with Canonicity

Anthony Cantor, Aaron Stump

09:00-10:00

Invited Talk: Looking Backward; Looking Forward

Dana Scott

10:00-10:30

A Brouwerian proof of the Fan Theorem

Michael Fourman

09:00-10:00

TBA

Samson Abramsky

10:00-10:30

"Operational'' Game Semantics

Radha Jagadeesan

09:00-10:00

Homotopy coherent adjunctions and other structures

Emily Riehl

10:00-10:30

Merge-bicategories: towards semi-strictification of higher categories

Amar Hadzihasanovic

09:00-10:00

On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification

Naoki Kobayashi

09:00-10:00

Confluence in Constraint Handling Rules: An overview from early, fundamental results to recent extensions including state invariants and conf. modulo

Henning Christiansen, Maja Hanne Kirkeby

10:00-10:30

Coherence modulo relations

Benjamin Dupont, Philippe Malbos

09:00-10:00

Invited talk: Cubical Computational Type Theory and RedPRL

Kuen-Bang Hou Favonia

10:00-10:30

Sharing a library between proof assistants: reaching out to the HOL family

François Thiré

09:00-09:30

Asynchronous games fifteen years later

Paul-André Melliès

09:30-10:30

Algebraic Theories and Control Effects, Back and Forth

Marcelo Fiore

09:00-09:20

Substructural Calculi with Dependent Types

Zhaohui Luo

09:20-09:55

On the Lambek Calculus with an Exchange Modality

Jiaming Jiang, Harley Eades Iii, Valeria de Paiva

09:55-10:30

The Bang Calculus and the Two Girard's Translations

Giulio Guerrieri, Giulio Manzonetto

09:00-10:00

Is compositionality all it's cracked up to be?

Ann Copestake

10:00-10:30

Anti-Unification and Natural Language Processing

Nino Amiridze, Temur Kutsia

09:00-09:15

Workshop introduction

David Baelde, Alexis Saurin

09:15-10:30

An Introduction to Cyclic Proofs

James Brotherston

09:00-09:30

Tuning Parallel SAT Solvers

Thorsten Ehlers, Dirk Nowotka

09:30-10:00

CryptoMiniSat Parameter-Optimization for Solving Cryptographic Instances

Anastasia Leventi-Peetz, Oliver Zendel, Werner Lennartz, Kai Weber

10:00-10:30

Stedman and Erin Triples encoded as a SAT Problem

Andrew Johnson

09:00-10:30

Strategic behavior in social choice - Part 1

Edith Elkind

09:00-10:00

An introduction to deep inference

Willem Heijltjes

10:00-10:30

Deep-Inference Intersection Types

Joseph Paulus, Willem Heijltjes

09:00-10:00

Handling substitutions via duality

Silvio Ghilardi

10:00-10:30

Unification based on generalized embedding

Joerg Siekmann, Peter Szabo

09:30-10:30

Axiomatizing Cubical Sets Models of Univalent Foundations

Andrew Pitts

09:30-10:30

Critical Pairs in Graph Transformation Systems

Fernando Orejas

10:00-10:30

Combinatorics of explicit substitutions (extended abstract)

Maciej Bendkowski, Pierre Lescanne

11:00-11:45

Fast cut-elimination using proof terms: an empirical study

Gabriel Ebner

11:45-12:30

Validating Back-links of FOL-ID Cyclic Pre-proofs

Sorin Stratulat

11:00-11:30

Invited Talk: A Brief History of Denotational Semantics

Stephen Brookes

11:30-12:00

First-order differential programming

Gordon Plotkin

12:00-12:30

Games and domains

Glynn Winskel

11:00-11:30

Some reflections on algorithmic game semantics

Pasquale Malacaria

11:30-12:30

Strategies as sheaves on plays

Luke Ong

11:00-11:30

The equivalence between opetopic sets and many-to-one polygraphs

Cédric Ho Thanh

11:30-12:00

Minimal models for monomial algebras

Pedro Tamaroff

12:00-12:30

Termination in linear (2,2)-categories with braidings and duals

Benjamin Dupont

11:00-12:00

Some applications of quantitative types inside and outside type theory

Pierre Vial

11:00-11:30

Internalizing Presheaf Semantics: Charting the Design Space

Andreas Nuyts, Dominique Devriese

11:30-12:00

Cubical Assemblies and the Independence of the Propositional Resizing Axiom

Taichi Uemura

12:00-12:30

Dependent Right Adjoint Types

L. Birkedal, R. Clouston, B. Mannaa, R. Møgelberg, A. Pitts, B. Spitters

11:00-11:30

Coherence of monoids by insertions

Nohra Hage, Philippe Malbos

11:30-12:00

Critical pairs for Gray categories

Simon Forest

12:00-12:30

The diamond lemma for free modules

Cyrille Chenavier

11:00-12:00

Invited talk: Why and How Does K work? The Logical Infrastructure Behind It

Grigore Rosu

12:00-12:20

Computation-as-deduction in Abella: work in progress

Kaustuv Chaudhuri, Ulysse Gérard, Dale Miller

12:20-12:40

Property-Based Testing of Abstract Machines: an Experience Report

Francesco Komauli, Alberto Momigliano

11:00-11:30

A more precise, more correct stack and register model for CompCert

Gergö Barany

11:30-12:00

Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear

Yannick Forster, Dominique Larchey-Wendling

12:00-12:30

A graph-rewriting perspective of the beta-law

Dan R. Ghica, Koko Muroya, Todd Waugh Ambridge

11:00-12:00

Termination of lambda-calculus linearization methods

Sandra Alves

12:00-12:35

Taking Linear Logic Apart

Wen Kokke, Fabrizio Montesi, Marco Peressotti

11:00-11:30

Propositional Attitude Operators in Homotopy Type Theory

Colin Zwanziger

11:30-12:00

Propositional Forms of Judgemental Interpretations

Tao Xue, Zhaohui Luo, Stergios Chatzikyriakidis

12:00-12:30

Paychecks, Presupposition, and Dependent Types

Ribeka Tanaka, Koji Mineshima, Daisuke Bekki

11:00-11:45

Local Validity for Circular Proofs in Linear Logic with Fixed Points

Rémi Nollet

11:45-12:30

Collapses of Fixpoint Alternation Hierarchies in Low Type-Levels of Higher-Order Fixpoint Logic

Florian Bruse, Martin Lange, Etienne Lozes

11:00-11:30

Two flavors of DRAT

Adrian Rebola Pardo, Armin Biere

11:30-12:00

Competitive Sorter-based Encoding of PB-Constraints into SAT

Michał Karpiński, Marek Piotrów

12:00-12:30

Divide and Conquer: Towards Faster Pseudo-Boolean Solving

Jan Elffers, Jakob Nordstrom

11:00-12:30

Strategic behavior in social choice - Part 2

Edith Elkind

11:00-11:30

Drags: an algebraic framework for graph rewriting

Nachum Dershowitz, Jean-Pierre Jouannaud

11:30-12:00

A framework for rewriting families of string diagrams

Vladimir Zamdzhiev

12:00-12:30

On quasi ordinal diagram systems

Mitsuhiro Okada, Yuta Takahashi

11:00-11:30

Truely Concurrent Processes in the Calculus of Structures

Ross Horne

11:30-12:00

Sequentialising nested systems

Bjoern Lellmann, Elaine Pimentel, Revantha Ramanayake

12:00-12:30

Nested sequents for modal logics and beyond

Sonia Marin

11:00-11:30

Knowledge Problems in Equational Extensions of Subterm Convergent Theories

Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen

11:30-12:00

Bounded ACh Unification

Ajay Kumar Eeralla, Christopher Lynch

12:00-12:30

About the unification type of topological logics over Euclidean spaces

Çigdem Gencer

12:00-12:30

Orthogonality and sequentiality in substructural Linear HRSs

Connor Smith

14:00-14:45

On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant

Federico Aschieri

14:45-15:15

Herbrand's Theorem as Higher-Order Recursion

Graham Leigh

14:00-14:40

Invited Talk: Scott Domains for Denotational Semantics and Program Extraction

Ulrich Berger

14:40-15:05

Robust computability notions for types arising in classical analysis

John Longley

15:05-15:30

T^\omega-representations of compact sets through dyadic subbases

Hideki Tsuiki, Arno Pauly

14:00-14:30

Game semantics: from call-by-push-value and CPS to coalgebra

Paul Levy

14:30-15:00

Incomplete information and uniformity in game semantics

Guy McCusker

15:00-15:30

Asynchronous games fifteen years later

Paul-André Melliès

14:00-15:00

A homotopy type theory for directed homotopy theory

Paige North

14:00-15:00

A homotopy type theory for directed homotopy theory

Paige North

14:00-15:00

Wanda: a higher-order termination tool

Cynthia Kop

14:00-14:30

Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs

Naoki Nishida, Yuta Tsuruta, Yoshiaki Kanazawa

14:30-15:00

Towards a Verified Decision Procedure for Confluence of Ground Term Rewrite Systems in Isabelle/HOL

Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp

15:00-15:30

Certified Ordered Completion

Christian Sternagel, Sarah Winkler

14:00-14:30

Formalization in Constructive Type Theory of the Standardization Theorem

Matrín Copes, Nora Szasz, Alvaro Tasistro

14:30-15:00

Formalisation of Barendregt's Variable Convention for Generic Structures with Binders

Ernesto Copello, Nora Szasz, Alvaro Tasistro

15:00-15:20

What Does This Notation Mean Anyway? BNF-style notation as it is actually used

David Feller, Joe Wells, Sébastien Carlier, Fairouz Kamareddine

14:00-14:20

The structure of non decomposable connectives of linear logic

Roberto Maieli

14:20-14:55

On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants

Lionel Vaux Auclair, Federico Olimpieri

14:55-15:30

From Linear Logic to Cyclic Sharing

Masahito Hasegawa

14:00-15:00

Speakers in vats: simulating model-theoretic alignment with distributional semantics

Aurelie Herbelot

15:00-15:30

Graph Knowledge Representations for SICK

Aikaterini-Lida Kalouli, Richard Crouch, Valeria de Paiva, Livy Real

14:00-14:45

Useless Explicit Induction Reasoning

Sorin Stratulat

14:45-15:30

Towards the Automatic Construction of Schematic Proofs

David Cerna, Michael Lettmann

14:00-15:00

Space Proof Complexity beyond Resolution

Nicola Galesi

15:00-15:30

Branching Program Complexity of Canonical Search Problems and Proof Complexity of Formulas

Alexander Knop

14:00-14:40

Compositional Game Theory

Neil Ghani, Jules Hedges, Philipp Zahn, Viktor Winschel

14:40-15:20

Concurrent games and semi-random determinacy

Stephane Le Roux

14:00-15:00

Modeling terms by graphs with structure constraints (two illustrations)

Clemens Grabmayer

15:00-15:30

Semantics-Preserving DPO-Based Term Graph Rewriting

Wolfram Kahl, Yuhang Zhao

14:00-15:00

Two Unifying Structural Principles

Alessio Guglielmi

15:00-15:30

Deep Inference, Herbrand's Theorem and Expansion Proofs

Benjamin Ralph

14:00-15:00

Compressed Term Unification: Results, uses, open problems, and hopes

Adrià Gascón

15:00-15:30

ACUI Unification modulo Ground Theories

Franz Baader, Pavlos Marantidis, Antoine Mottet

14:30-15:30

Invited talk: Semantic Equivalence Checking for HHVM Bytecode

Nick Benton

14:30-15:00

Local-Style Search in the Linear MaxSAT Algorithm: A Computational Study of Solution-Based Phase

Emir Demirović, Peter J. Stuckey

15:00-15:30

MLIC: A MaxSAT-Based framework for learning interpretable classification rules

Dmitry Malioutov, Kuldeep S. Meel

15:00-15:30

Towards a fully formalized definition of syllepsis in weak higher categories

Thibaut Benjamin

15:00-15:30

Refining Properties of Filter Models: Sensibility, Approximability and Reducibility

Flavien Breuvart

15:00-15:30

Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT

Genki Sato

16:00-16:30

Admissible tools in the kitchen of intuitionistic logic

Matteo Manighetti, Andrea Condoluci

16:30-17:00

The “duality of computation” from a fibrational perspective

Nuria Brede

17:00-17:30

A Denotational Model of the Typed Lambda-Mu Calculus

Ken Akiba

17:30-18:00

Some ideas on cut-elimination for cyclic arithmetic proofs

Anupam Das

16:00-16:25

Higher-dimensional categories: recursion on extensivity

Thomas Cottrell, Soichiro Fujii, John Power

16:25-16:50

A logical view of complex analytic maps

Abbas Edalat, Mehrdad Maleki

16:00-16:30

Games and the Lambda Cube

James Laird

16:30-17:00

Games, Geometry of Interaction, Reversible Computations, Lambda Calculus

Marina Lenisa

17:00-17:30

Characterizing observational equivalence for PCF terms within richer languages

John Longley

16:00-16:30

Minimal Bacus FP is Turing Complete

Richard Statman

16:30-17:00

String data structures for Chinese monoids

Nohra Hage

17:00-17:30

Generalizations of the associative operad and convergent rewrite systems

Cyrille Chenavier, Christophe Cordero, Samuele Giraudo

17:30-18:00

Normal forms for planar connected string diagrams

Antonin Delpeuch, Jamie Vicary

16:00-16:30

Normalization and Taylor expansion of lambda-terms

Federico Olimpieri

16:30-17:00

The next 700 (type-theoretical) denotational models ?

Damiano Mazza, Domenico Ruoppolo

16:00-16:30

Univalent Foundations and the Constructive View of Theories

Andrei Rodin

16:30-17:00

Algebraic models of dependent type theory

Clive Newstead

17:00-17:30

First-order homotopical logic and Grothendieck fibrations

Joseph Helfer

16:00-16:30

Complete Axiom System of Cluster Algebra

Kousuke Fukui, Koji Nakazawa

16:30-17:30

IWC Business Meeting

Nao Hirokawa, Aart Middeldorp

16:00-17:00

Invited talk: A fresh view of call-by-need

Delia Kesner

17:00-17:30

Abstract Representation of Binders in OCaml using the Bindlib Library

Rodolphe Lepigre, Christophe Raffalli

17:30-17:50

Functional programming with λ-tree syntax: a progress report

Ulysse Gérard, Dale Miller

16:00-16:30

Denotational Event structure for relaxed memory

Jade Alglave, Simon Castellan, Jean-Marie Madiot

16:30-17:00

A resource modality for RAII

Guillaume Combette, Guillaume Munch-Maccagnoni

17:00-17:30

Experimenting with graded monads: certified grading-based program transformations

Tõnn Talvik, Tarmo Uustalu

17:30-18:00

Heaps denote finitely partitioned trees

Paul Blain Levy

16:00-17:00

Applying linear logic semantics to probabilistic programming

Michele Pagani

17:00-17:35

Proof nets, coends and the Yoneda isomorphism

Paolo Pistone

17:35-18:10

Quantum programming made easy

Luca Paolini, Luca Roversi, Margherita Zorzi

16:00-16:30

Automated Reasoning from Polarized Parse Trees

Hai Hu, Thomas Icard, Larry Moss

16:30-17:00

Do different syntactic trees yield different logical readings? Some remarks on head variables in typed lambda

Davide Catta, Richard Moot, Christian Retoré

17:00-17:30

Automatic test suite generation for PMCFG grammars

Inari Listenmaa, Koen Claessen

17:30-18:00

OpenWordNet-PT: Taking Stock

V. de Paiva, A. Rademaker, L. Real, F. Chalub, G. de Melo

16:00-17:15

The size-change principle and circular proofs: checking totality of (co)recursive definitions

Pierre Hyvernat

17:15-18:00

What makes guarded types tick?

Patrick Bahr, Bassel Mannaa, Rasmus Ejlers Møgelberg

16:00-17:00

On OBBD Proofs

Sam Buss

17:00-17:20

Resolution and the binary encoding of combinatorial principles

Stefan Dantchev, Nicola Galesi, Barnaby Martin

17:20-17:40

Resolution with Counting: Different Moduli and Tree-Like Lower Bounds

Fedor Part, Iddo Tzameret

17:40-18:10

Proof systems for #SAT based on restricted circuits

Florent Capelli

16:00-16:30

A Problem Meta-Data Library for Research in SAT

Markus Iser, Carsten Sinz

16:30-17:00

The Effect of Scrambling CNFs

Armin Biere, Marijn Heule

17:00-17:30

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

Jan Elffers, Jesus Giráldez-Cru, Stephan Gocht, Jakob Nordstrom, Laurent Simon

17:30-17:45

On the use of solvers with docker technology

Daniel Le Berre

17:45-18:00

Questions and Answers

Matti Järvisalo

16:00-16:40

Verification of Multi-agent Systems with Imperfect Information and Public Actions

Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, Sasha Rubin

16:40-17:20

Local Equilibria in Logic-Based Multi-Player Games

Julian Gutierrez, Paul Harrenstein, Thomas Steeples, Michael Wooldridge

17:20-18:00

Beyond admissibility: Dominance between chains of strategies

N. Basset, I. Jecker, A. Pauly, J.-F. Raskin, M. Van Den Bogaard

16:00-16:30

SLD-Resolution Reduction of Second-Order Horn Fragments - Extended Abstract

Sophie Tourret, Andrew Cropper

16:30-17:00

A Port-graph Model for Finance

Nneka Ene

17:00-17:30

Finding the Transitive Closure of Functional Dependencies using Strategic Port Graph Rewriting

János Varga

17:30-18:00

Programming by Term Rewriting

Lee Barnett, David Plaisted

16:00-17:00

Some incoherent musings on deep inference and combinatorial proofs

Dominic Hughes

17:00-18:00

Proof complexity of deep inference: a survey

Anupam Das

16:00-16:30

Proximity-Based Generalization

Cleo Pau, Temur Kutsia

16:30-17:00

Towards Generalization Methods for Purely Idempotent Equational Theories

David Cerna, Temur Kutsia

17:00-17:30

Rewriting with Generalized Nominal Unification

Yunus David Kerem Kutz, Manfred Schmidt-Schauss

17:30-17:50

Formalization of First-Order Syntactic Unification

Kasper Fabæch Brandt, Anders Schlichtkrull, Jørgen Villadsen

17:50-18:10

Efficiency of a good but not linear nominal unification algorithm

Weixi Ma, Jeremy Siek, David Christiansen, Daniel Friedman

17:00-18:00 Remembering Klaus Keimel

17:00-18:00 Special session in honour of Kris Rose

18:10-18:40 UNIF 2018 Wrap Up

19:00-21:00 UNIF Dinner

19:00-21:00 LFMTP Dinner

10:30-11:00 Coffee Break

12:30-14:00 Lunch Break

15:30-16:00 Coffee Break

19:45-22:00 Workshops dinner at Balliol College