FLoC on Saturday, July 10th

See also the by session program.

DCM	DTP	HyLo	IFIP-WG1.6	LCC	LSB	LoCoCo	POS	PSPL
09:00‑10:00 Vlatko Vedral (Oxford University) Phase Estimation with Mixed States: Quantum Coherence versus Correlations	09:00‑10:00 Matthieu Sozeau (Harvard University) Elaborations in Type Theory	09:00‑09:30 Dario Della Monica, Valentin Goranko and Guido Sciavicco Hybrid Metric Propositional Neighborhood Logics with Interval Length Binders 09:30‑09:50 Michael R. Hansen Efficient Model Checking for a Hybrid Duration Calculus	09:00‑09:30 Kristoffer Rose Compromising Rewriting (Abstract) 09:30‑10:00 Beniamino Accattoli and Delia Kesner The structural lambda-calculus	09:00‑10:00 Ugo Dal Lago Implicit Complexity in a Concurrency Scenario	09:00‑10:00 Marta Kwiatkowska (University of Oxford) Probabilistic Model Checking for Systems Biology	09:00‑10:00 Carsten Sinz (University of Karlsruhe) Software Configuration: What can we learn from Product Configuration?	09:00‑10:00 Youssef Hamadi (Microsoft Research) From Parallel SAT to Distributed SAT	09:00‑10:00 Invited Talk: Viktor Vafeiadis Recent developments in concurrent program logics
10:00‑10:30 Coffee break
10:30‑11:00 Bas Spitters Spitters The space of measurement outcomes as a non-commutative spectrum 11:00‑11:30 Mio Murao and Akihito Soeda Delocalization power of global unitary operations on quantum information 11:30‑12:30 Cristian Calude (University of Auckland, New Zealand) Understanding the Quantum Computational Speed-up via De-quantisation	10:30‑11:00 Adam Chlipala (Harvard University) Generating Pieces of Web Applications with Type-Level Programming 11:00‑11:30 Larry Diehl Unit & integration test composition via lemmas 11:30‑12:00 Sean Wilson (University of Edinburgh) Supporting Dependently Typed Functional Programming with Proof Automation and Testing 12:00‑12:30 Karim Kariso (University of Swansea) Integrating Agda and Automated Theorem Proving Techniques	10:30‑11:30 Moshe Vardi (Rice University) Hybrid Logic: The Search for The Decidability Frontier 11:30‑12:00 Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas and Felix Weiss The Complexity of Satisfiability for Fragments of Hybrid Logic --- Part II 12:00‑12:30 Jens Ulrik Hansen A Hybrid Public Announcement Logic with Distributed Knowledge	10:30‑11:00 Georg Moser Complexity Analysis of Programs by Rewriting 11:00‑11:30 Salvador Lucas Matrix interpretations over the rationals and matrix interpretations over the naturals 11:30‑12:00 Bernhard Gramlich Conditional via Unconditional Rewriting - Some Recent Developments 12:00‑12:30 Hans Zantema Proving equality of infinite terms: co-inductive theorem proving	10:30‑11:00 Guillaume Bonfante Course of value in programming languages 11:00‑11:30 Stephen Cook and Lila Fontes Formal Theories for Linear Algebra 11:30‑12:00 Marco Gaboardi and Brian Redmond Towards a Light Logic for PSPACE 12:00‑12:30 Pierre Boudes, Damiano Mazza and Lorenzo Tortora de Falco A Categorical Construction for Linear Logic by Levels	10:30‑11:30 Peter Gennemark (University of Gothenburg and Uppsala University) Modelling Yeast Osmoregulation at Different Levels of Resolution 11:30‑12:30 Ion Petre (Åbo Akademi University) Molecular Self-Assembly Models of Variable Resolution	10:30‑11:00 Claude Michel and Michel Rueher Handling software upgradeability problems with MILP solvers 11:00‑11:30 Josep Argelich, Daniel Le Berre, Ines Lynce, Joao Marques-Silva and Pascal Rapicault Solving Linux Upgradeability Problems Using Boolean Optimization 11:30‑12:00 Paulo Trezentos Comparison of PBO solvers in a dependency solving domain 12:00‑12:30 Emmanuel Ohayon, Matthieu Lemerre and Vincent David CONFIGEN: A tool for management of configuration options	10:30‑11:00 Adrian Kuegel Improved Exact Solver for the Weighted MAX-SAT Problem 11:00‑11:30 Carlos Ansótegui, María Luisa Bonet and Jordi Levy On Solving MaxSAT Through SAT 11:30‑12:00 Daniel Le Berre and Anne Parrain The SAT4J library 2.2, System Description 12:00‑12:30 Mate Soos Enhanced Gaussian Elimination in DPLL-based SAT Solvers	10:30‑11:00 Luís Caires, Carla Ferreira and António Ravara A simple proof system for lock-free concurrency 11:00‑11:30 Giuseppe Primiero A multi-modal dependent type theory for representing data accessibility in a network 11:30‑12:00 Sungwoo Park and Jonghyun Park Towards a Cut-free Sequent Calculus for Boolean BI 12:00‑12:30 Holger Gast A Developer-oriented Hoare Logic
12:30‑14:00 Lunch
14:00‑15:00 Lucien Hardy (Perimeter Institute for Theoretical Physics) Operational Computing with Quantum Stuff	14:00‑14:30 Cezar Ionescu (Potsdam Institute for Climate Impact Research) Using dependent types in models of climate change impacts 14:30‑15:00 Hugo Herbelin (INRIA) A sequent calculus presentation of the Calculus of Inductive Constructions	14:00‑15:00 Gert Smolka (Saarland University) Tableau-Based Decision Procedures for Hybrid Logic	14:00‑14:30 Maribel Fernandez PORGY: a strategy driven interactive environment for visualisation and transformation of graphs 14:30‑15:00 Tetsuo Ida Graph Rewriting in Computational Origami	14:00‑15:00 Stephen Cook Bounded Reverse Mathematics	14:00‑15:00 Jasmin Fisher (Microsoft Research Cambridge) Bio-Logic: The Challenges Facing Formal Modelling of Biology	14:00‑14:30 Andreas Kübler, Christoph Zengler and Wolfgang Küchlin Model Counting in Product Configuration 14:30‑15:00 Roberto Di Cosmo and Ralf Treinen (Université Paris-Diderot) Result of the MISC Competition	14:00‑14:30 Norbert Manthey and Ari Saptawijaya Towards Improving the Resource Usage of SAT-solvers 14:30‑15:00 Adrian Balint, Daniel Gall, Gregor Kapler and Robert Retz Experiment design and administration for computer clusters for SAT-solvers (EDACC)	14:00‑15:00 Invited Talk: André Platzer Proof Systems for Hybrid System Logics
15:00‑15:30 Coffee break
15:30‑16:00 Dominik Floess, Erika Andersson and Mark Hillery Quantum algorithms for testing Boolean functions 16:00‑16:30 Vedran Dunjko and Elham Kashefi Algebraic characterization of one-way patterns 16:30‑17:00 Lucas Dixon, Ross Duncan and Aleks Kissinger Open Graphs and Computational Reasoning 17:00‑17:30 Abolfazl Bayat, Pasquale Sodano and Sougato Bose Entanglement in the Kondo Spin Chain 17:30‑18:00 Janet Anders, Stefanie Hilt, Saroosh Shabbir and Eric Lutz Landauer’s principle in the quantum domain	15:30‑16:00 Makoto Hamana (University of Gunma) Another Initial Algebra Semantics of Inductive Families for Programming 16:00‑16:30 Tarmo Uustalu (Institute of Cybernetics, Tallinn) Safely navigable datastructures with cycles and sharing 16:30‑17:00 Ulf Norell (Chalmers University) Lightweight reflection in Agda	15:30‑15:50 Valeria de Paiva, Hermann Hausler and Alexandre Rademaker Constructive Description Logic, Hybrid-Style 15:50‑16:10 Søren Lind Kristiansen and Anders Søgaard Querying dependency treebanks using hybrid logic 16:10‑16:30 Katsuhiko Sano Axiomatizing Hybrid Products of Monotonic Neighborhood Frames 16:30‑16:50 Thomas Bolander Two approaches to termination and completeness for hybrid tableaus	15:30‑16:00 Temur Kutsia Parameterized Generalization of Unranked Terms 16:00‑16:30 Helene Kirchner Operational Specification and Verification of Security Policies 16:30‑17:00 Maria Paola Bonacina Research activities related to term rewriting at the Universita` degli Studi di Verona 17:00‑17:15 Vincent van Oostrom. Report on ISR 2010 and Discussion on ISR 17:15‑17:30 Business Meeting	15:30‑16:30 Albert Atserias On Spectral Methods as Refutation Heuristic 16:30‑17:00 Alexander Rabinovich Temporal logics over linear time domains are in PSPACE 17:00‑17:30 Jiamou Liu Recursion-Theoretic Complexity of \omega-Automatic Trees	15:30‑16:30 John K. Heath (University of Birmingham) Protein Computing: a Phospho-Calculus? 16:30‑17:30 Steven Watterson (University of Edinburgh) Signalling Pathway Logic in the Immune Response. How Can We Make Complex Problems More Tractable?		15:30‑16:00 Florian Lonsing and Armin Biere DepQBF: A Dependency-Aware QBF Solver 16:00‑16:30 Luca Pulina and Armando Tacchella AQME'10 System Description 16:30‑17:00 Enrico Giunchiglia, Massimo Narizzano and Paolo Marin QuBE7.0, System Description	15:30‑16:00 Matteo Mio A Proof System for Reasoning about Probabilistic Concurrent Processes 16:00‑17:00 Discussion Session: Peter O'Hearn and Alex Simpson Challenge topics in PSPL