The overall aim of the Ticamore project is to systematically study the relationships between internal and external calculi for several families of important logics (classical, intuitionistic and epistemic modal logics, substructural logics, bunched implication logics and their modal extensions, conditional logics). Further aims include the construction of new internal calculi for logics of interest with the intention of investigating properties including decidability and complexity, conservativity, axiomatisations and interpolation; the development of prototype implementations of various calculi for countermodel generation and practical tools to automate the translation of proofs between calculi.
The web site is https://ticamore.logic.at.
A diagrammatic language for Quantum Reasoning: The ZX-calculus
The ZX-calculus is a language based on categorical logic used to make proofs on quantum circuits, and that can be interpreted as some kind of equational logic for graphs. In this talk, I will present the motivations for this language, its syntax and its original set of rules, as well as the recent results from Loria and Oxford giving a complete axiomatisation of relevant fragments of the language.
DEEPSEC: Deciding Equivalence Properties in Security Protocols
Automated verification has become an essential part in the security evaluation of cryptographic protocols. Recently, there has been a considerable effort to lift the theory and tool support that existed for reachability properties to the more complex case of equivalence properties. In this talk I will report on our recent advances in theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and provide a decision procedure for these equivalences in the case of a bounded number of sessions. Our procedure is the first to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives -- those that can be represented by a subterm convergent destructor rewrite system. We implemented the procedure in a new tool, DEEPSEC. We showed through extensive experiments that it is significantly more efficient than other similar tools, while at the same time raises the scope of the protocols that can be analysed.
Internalizing Labelled Proofs for Tense Logics with Path Axioms
We begin with a Negri-style labelled calculus for the tense logic Kt with structural rules corresponding to path axioms. Through the addition of special rules, referred to as "propagation rules," we can prove that the Negri-style structural rules are admissible in the resulting calculus. Every proof of a formula in this calculus contains sequents whose structure corresponds to a tree with two types of edges. This specific structure allows us to translate these proofs into display proofs for the same class of logics, which gives an answer to an open question of translating labelled proofs to display proofs for extensions of the minimal tense logic Kt.
Internal and external calculi for Intutionistic Non Normal Modal Logic
We propose a minimal non-normal intuitionistic modal logic. We discuss internal and external calculi for it, Hibert axiomatisation and possible semantic interpretations.
The logic of condtional beliefs: internal and labelled calculi
We present some calculi for the logic of Conditional beliefs in both the single and multi agent case. For the single agent case, we can provide a simple hypersequent calculus. In the multi-agent case a nested calculus is needed. We also present a natural labelled calculus for it. We discuss translations between calculi.
Translations of LBI proofs into GBI proofs in BI logic
In order to study proof translations in BI logic, we consider the bunched sequent calculus LBI and then define a new labelled sequent calculus, called GBI. We propose a procedure that translates LBI proofs into GBI proofs and prove its soundness. Moreover we discuss some steps towards the reverse translation of GBI proofs into LBI proofs and propose an algorithm that is illustrated by some examples.
Getting rid of tableau labels through hybridation
We consider Hybrid BBI logic (HBBI) and then present a tableaux calculus for this logic. Then we study the relationships between this new calculus and the labelled tableaux calculus for BBI logic. We mainly focus on the translations between HBBI tableaux proofs and BBI tableaux proofs that are illustrated with significant examples.
Separation Logic with One Quantified Variable
We investigate first-order separation logic with one record field restricted to a unique quantified variable (1SL1). Undecidability is known when the number of quantified variables is unbounded and the satisfiability problem is PSPACE-complete for the propositional fragment. We show that the satisfiability problem for 1SL1 is PSPACE-complete and we characterize its expressive power by showing that every formula is equivalent to a Boolean combination of atomic properties. This contributes to our understanding of fragments of first-order separation logic that can specify properties about the memory heap of programs with singly-linked lists. All the fragments we consider contain the magic wand operator and first-order quantification over a single variable.
The third TICAMORE meeting will take place at the LORIA laboratory in Nancy, France.
Nancy, located about 300km east of Paris, is at 1:30 hours by TGV from Paris. There are direct trains to Nancy station from Paris-Est. Other TGV trains connect Paris CDG airport and other major French cities with the TGV Lorraine train station, located about 40km from Nancy, which is reached by shuttle bus in about 40 minutes. Other trains reach Nancy from Strasbourg (and Switzerland and the south of Germany) and from Luxembourg and Metz (linking Nancy with Benelux and Germany). Consult the DB Web site for train connections to Nancy from within Europe.
By plane, Nancy is best reached through Paris CDG or Orly airports. From Paris CDG, you can catch a direct train to the TGV Lorraine station and then continue by shuttle bus. From Paris CDG or Orly, you can take the RER B to Gare du Nord, walk or take the Metro 4 to Gare de l'Est and take a TGV to Nancy train station. Luxembourg airport can be convenient as well: take the bus to Luxembourg train station, from which there are frequent connections to Nancy.
Alternatives are Frankfurt or Strasbourg airports. Low-cost flights reach Basel-Mulhouse or Frankfurt-Hahn, but it can be more difficult to reach Nancy from these airports by public transportation. Metz-Nancy regional airport is located close to the TGV Lorraine station and is served by the same shuttle buses.
LORIA is located on the campus of the Faculty of Sciences of Nancy University (Université de Lorraine). Its physical address is
615 rue du Jardin Botanique
54602 Villers-lès-Nancy
tel. (+33) 383 59 30 00
See conference venue, tram line and stop on TICAMORE Google map
From the train station, LORIA is easily reached by bus or by tram.
Access by bus: the Campus line (also known as 128) from the "Nancy Gare" stop in the direction of "Vandoeuvre CHU - Stan Campus" and get off at the stop "Grande Corvée". LORIA is on your left, walk uphill about 30m. (The bus stop is in Rue du Jardin Botanique, facing the back side of LORIA, the main entrance to LORIA is on the other side.) The bus ride takes less than 15 minutes, buses run every 8-15 minutes during working hours.
Access by tram: Take the T1 line at the "Nancy Gare" stop in the direction of "Vandoeuvre CHU" and get off at the stop "Callot". Then traverse the University campus (see map below): from the tram stop, go right in the direction of Lycée Jacques Callot, then follow the street uphill (turning left), finally enter the campus. LORIA is the white building on the top of the hill. The tram takes less than 15 minutes and runs approximately every 7-15 minutes during working hours.
There are many hotels both downtown and closer to the venue, with very moderate prices (about 60 ¤ per night). Here is a selection of some hotels in Nancy, which are located close to the city center and the tram and bus lines to the Inria Nancy research Center:
For more options, see Office de tourisme or http://www.booking.com.