The workshop will be held at\u00a0the Departamento de Computaci\u00f3n of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!<\/p>\n
10:00-10:15 Sergio Yovine and Eduardo Bonelli<\/strong> 10:15-10:50\u00a0Diego Figueira (CNRS,LaBRI, France)<\/strong> 10:50-11:25\u00a0Flavia Bonomo (UBA,CONICET)<\/strong> 11:25-11:40 Coffee break<\/strong><\/p>\n 11:40-12:15\u00a0Alejandro D\u00edaz-Caro (UNQ)<\/strong> 12:15-12:50\u00a0Beta Ziliani (FAMAF, CONICET)<\/strong> 12:50-14:00 Lunch<\/strong><\/p>\n 14:00-14:35\u00a0Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)<\/strong> 14:35-15:10\u00a0Thibaut Balabonski (INRIA, U. Paris Sud)<\/strong> 15:10-15:25 Coffee break<\/strong><\/p>\n 15:25-16:00\u00a0Juan Pablo Galleoti (UBA, CONICET)<\/strong> 16:00-16:15\u00a0Sergio Yovine and Eduardo Bonelli Diego Figueira (CNRS,LaBRI, France)<\/strong> The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.<\/p>\n Flavia Bonomo (UBA,CONICET)<\/strong> We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time.\u00a0While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4). Alejandro D\u00edaz-Caro (UNQ)<\/strong> By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.<\/p>\n Beta Ziliani (FAMAF, CONICET)<\/strong> Proof assistants like Coq are now eminently effective for formalizing\u00a0“research-grade” mathematics, verifying serious software systems, and,\u00a0more broadly, enabling researchers to mechanize and breed confidence\u00a0in their results. Nevertheless, the mechanization of substantial\u00a0proofs typically requires a significant amount of manual effort. To\u00a0alleviate this burden, proof assistants typically provide an\u00a0additional language for tactic programming. Tactics support\u00a0general-purpose scripting of automation routines, as well as fine\u00a0control over the state of an interactive proof. However, for most\u00a0existing tactic languages (e.g., ML, Ltac), the price to pay for this\u00a0freedom is that the behavior of a tactic lacks any static\u00a0specification within the base logic of the theorem prover (such as, in\u00a0Coq, a type). As a result of being untyped, tactics are known to be\u00a0difficult to compose, debug, and maintain.<\/p>\n In my thesis I developed two different approaches to typed tactic\u00a0programming in the context of Coq: Lemma Overloading and Mtac.\u00a0Both approaches rely heavily on the unification algorithm of Coq,\u00a0which is a complex mixture of different heuristics and has not been\u00a0formally specified. Therefore, I also build and describe a new\u00a0unification algorithm better suited for tactic programming in Coq. In\u00a0this talk I describe the high level achievements of my work and\u00a0introduce in depth Mtac, a new programming language for typed tactic\u00a0programming in Coq.<\/p>\n Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)<\/strong> We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\\mathcal K}(\\alpha)$ of the fractional parts of the multiples of a real $\\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\\mathcal K}(\\alpha)$,\u00a0and is useful to study the pseudo-randomness of the sequence ${\\mathcal K}(\\alpha)$ for a random input $\\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\\alpha$ is a random real, and the case when $\\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\\alpha$ plays an important r\u00f4le. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\\infty$ and the unconstrained case $M = \\infty$. Joint work with Brigitte Vall\u00e9e, CNRS and Universit\u00e9 de Caen,\u00a0France.<\/p>\n Thibaut Balabonski (INRIA, U. Paris Sud)<\/strong> Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler).\u00a0This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.<\/p>\n Juan Pablo Galleoti (UBA, CONICET)<\/strong> Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.<\/p>\n The workshop will be held at\u00a0the Departamento de Computaci\u00f3n of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!<\/p>\n 10:00-10:15\u00a0Sergio Yovine and Eduardo Bonelli<\/strong> 10:15-10:50\u00a0Diego Figueira (CNRS,LaBRI, France)<\/strong> 10:50-11:25\u00a0Flavia Bonomo (UBA,CONICET)<\/strong> 11:25-11:40\u00a0Coffee break<\/strong><\/p>\n 11:40-12:15\u00a0Alejandro D\u00edaz-Caro (UNQ)<\/strong> 12:15-12:50\u00a0Beta Ziliani (FAMAF, CONICET)<\/strong> 12:50-14:00\u00a0Lunch<\/strong><\/p>\n 14:00-14:35\u00a0Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)<\/strong> 14:35-15:10\u00a0Thibaut Balabonski (INRIA, U. Paris Sud)<\/strong> 15:10-15:25\u00a0Coffee break<\/strong><\/p>\n 15:25-16:00\u00a0Juan Pablo Galleoti (UBA, CONICET)<\/strong> 16:00-16:15\u00a0Sergio Yovine and Eduardo Bonelli Diego Figueira (CNRS,LaBRI, France)<\/strong> The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.<\/p>\n Flavia Bonomo (UBA,CONICET)<\/strong> We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time.\u00a0While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4). Alejandro D\u00edaz-Caro (UNQ)<\/strong> By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.<\/p>\n Beta Ziliani (FAMAF, CONICET)<\/strong> Proof assistants like Coq are now eminently effective for formalizing\u00a0“research-grade” mathematics, verifying serious software systems, and,\u00a0more broadly, enabling researchers to mechanize and breed confidence\u00a0in their results. Nevertheless, the mechanization of substantial\u00a0proofs typically requires a significant amount of manual effort. To\u00a0alleviate this burden, proof assistants typically provide an\u00a0additional language for tactic programming. Tactics support\u00a0general-purpose scripting of automation routines, as well as fine\u00a0control over the state of an interactive proof. However, for most\u00a0existing tactic languages (e.g., ML, Ltac), the price to pay for this\u00a0freedom is that the behavior of a tactic lacks any static\u00a0specification within the base logic of the theorem prover (such as, in\u00a0Coq, a type). As a result of being untyped, tactics are known to be\u00a0difficult to compose, debug, and maintain.<\/p>\n In my thesis I developed two different approaches to typed tactic\u00a0programming in the context of Coq: Lemma Overloading and Mtac.\u00a0Both approaches rely heavily on the unification algorithm of Coq,\u00a0which is a complex mixture of different heuristics and has not been\u00a0formally specified. Therefore, I also build and describe a new\u00a0unification algorithm better suited for tactic programming in Coq. In\u00a0this talk I describe the high level achievements of my work and\u00a0introduce in depth Mtac, a new programming language for typed tactic\u00a0programming in Coq.<\/p>\n Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)<\/strong> We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\\mathcal K}(\\alpha)$ of the fractional parts of the multiples of a real $\\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\\mathcal K}(\\alpha)$,\u00a0and is useful to study the pseudo-randomness of the sequence ${\\mathcal K}(\\alpha)$ for a random input $\\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\\alpha$ is a random real, and the case when $\\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\\alpha$ plays an important r\u00f4le. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\\infty$ and the unconstrained case $M = \\infty$. Joint work with Brigitte Vall\u00e9e, CNRS and Universit\u00e9 de Caen,\u00a0France.<\/p>\n Thibaut Balabonski (INRIA, U. Paris Sud)<\/strong> Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler).\u00a0This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.<\/p>\n Juan Pablo Galleoti (UBA, CONICET)<\/strong> Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.<\/p>\n The workshop will be held at\u00a0the Departamento de Computaci\u00f3n of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate!<\/p>\n 10:00-10:15\u00a0Sergio Yovine and Eduardo Bonelli<\/strong> 10:15-10:50\u00a0Diego Figueira (CNRS,LaBRI, France)<\/strong> 10:50-11:25\u00a0Flavia Bonomo (UBA,CONICET)<\/strong> 11:25-11:40\u00a0Coffee break<\/strong><\/p>\n 11:40-12:15\u00a0Alejandro D\u00edaz-Caro (UNQ)<\/strong> 12:15-12:50\u00a0Beta Ziliani (FAMAF, CONICET)<\/strong> 12:50-14:00\u00a0Lunch<\/strong><\/p>\n 14:00-14:35\u00a0Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)<\/strong> 14:35-15:10\u00a0Thibaut Balabonski (INRIA, U. Paris Sud)<\/strong> 15:10-15:25\u00a0Coffee break<\/strong><\/p>\n 15:25-16:00\u00a0Juan Pablo Galleoti (UBA, CONICET)<\/strong> 16:00-16:15\u00a0Sergio Yovine and Eduardo Bonelli Diego Figueira (CNRS,LaBRI, France)<\/strong> The talk will be centered on logics and automata models for data words and data trees. Data words and data trees are finite words and trees whose every position carries a pair (a,d), where ‘a’ is a label from a finite alphabet (eg the alphabet {a,b,c}), and ‘d’ is a data value from an infinite domain (eg the domain {1,2,3,…}). These structures arise naturally in the realm of databases, semistructured data, verification of temporal requirements, concurrency, and generally in verification of systems manipulating data values. I will comment on the general landscape of formalisms over these structures: the main techniques used, the decidability boundaries, connections with other areas, and some open problems.<\/p>\n Flavia Bonomo (UBA,CONICET)<\/strong> We present an algorithm to 3-colour an n-vertex graph without triangles or induced paths on seven vertices in O(n^7) time.\u00a0While this is a special case of the problem posed by Schiermeyer, Randerath and Tewes in 2002 and solved by Chudnovsky, Maceli, and Zhong in 2014, the algorithm here is both faster and conceptually simpler. Moreover, we solve a more general list-coloring problem, where every vertex is assigned a list of colours which is a subset of {1,2,3}. The complexity of the algorithm for this second problem in {P_7,triangle}-free graphs is again O(n^7), and if G is bipartite, it improves to O(n^4). Alejandro D\u00edaz-Caro (UNQ)<\/strong> By considering the quantum superposition as a non-idempotent conjunction, a projective measurement correspond to a non-deterministic projection over pairs. We propose an extension of simply typed lambda-calculus with pairs taking into account projective measurements, superposition with destructive interference and the no-cloning property of quantum computing. In this talk I will give a description of the system and the design choices, as well as an example of the Deutsch algorithm in this calculus. Joint work with Gilles Dowek.<\/p>\n Beta Ziliani (FAMAF, CONICET)<\/strong> Proof assistants like Coq are now eminently effective for formalizing\u00a0“research-grade” mathematics, verifying serious software systems, and,\u00a0more broadly, enabling researchers to mechanize and breed confidence\u00a0in their results. Nevertheless, the mechanization of substantial\u00a0proofs typically requires a significant amount of manual effort. To\u00a0alleviate this burden, proof assistants typically provide an\u00a0additional language for tactic programming. Tactics support\u00a0general-purpose scripting of automation routines, as well as fine\u00a0control over the state of an interactive proof. However, for most\u00a0existing tactic languages (e.g., ML, Ltac), the price to pay for this\u00a0freedom is that the behavior of a tactic lacks any static\u00a0specification within the base logic of the theorem prover (such as, in\u00a0Coq, a type). As a result of being untyped, tactics are known to be\u00a0difficult to compose, debug, and maintain.<\/p>\n In my thesis I developed two different approaches to typed tactic\u00a0programming in the context of Coq: Lemma Overloading and Mtac.\u00a0Both approaches rely heavily on the unification algorithm of Coq,\u00a0which is a complex mixture of different heuristics and has not been\u00a0formally specified. Therefore, I also build and describe a new\u00a0unification algorithm better suited for tactic programming in Coq. In\u00a0this talk I describe the high level achievements of my work and\u00a0introduce in depth Mtac, a new programming language for typed tactic\u00a0programming in Coq.<\/p>\n Eda Cesaratto (Instituto del Desarrollo Humano, Universidad Nacional de General Sarmiento and CONICET)<\/strong> We perform a probabilistic study of five parameters — two distances, covered space, discrepancy and Arnold measure– which describe the celebrated Kronecker sequence ${\\mathcal K}(\\alpha)$ of the fractional parts of the multiples of a real $\\alpha$. Each parameter can be viewed as a measure of randomness of the sequence ${\\mathcal K}(\\alpha)$,\u00a0and is useful to study the pseudo-randomness of the sequence ${\\mathcal K}(\\alpha)$ for a random input $\\alpha$. We wish to answer the question: Is a random Kronecker sequence pseudo-random (with respect to each randomness measure)? We consider two main cases: the case where the “”input”” $\\alpha$ is a random real, and the case when $\\alpha$ is a random rational, and we exhibit strong similarities between the two situations. It is already known that the size of the quotients in the continued fraction expansion of $\\alpha$ plays an important r\u00f4le. This is why we also focus to the “”constrained”” case where all the quotients are bounded by a constant $M$, and consider the transition between the constrained case $M<\\infty$ and the unconstrained case $M = \\infty$. Joint work with Brigitte Vall\u00e9e, CNRS and Universit\u00e9 de Caen,\u00a0France.<\/p>\n Thibaut Balabonski (INRIA, U. Paris Sud)<\/strong> Substantial research efforts have been devoted to tools for reasoning about -and proving properties of programs. A related concern is making sure that compilers preserve the soundness of programs, that is making sure that the compiled code respects the behavior of the source program (see for instance the CompCert C compiler).\u00a0This talk is about an attempt at proving the soundness of some basic low-level transformations for concurrent C programs. We will see some elements of the official semantics of concurrency in C, and I will relate how the focus of this work shifted from proving the soundness of program transformations to patching the official semantics.<\/p>\n Juan Pablo Galleoti (UBA, CONICET)<\/strong> Dynamic invariant detection allows mining of specifications from existing systems, but the quality of the resulting invariants depends on the executions observed: Unobserved behavior is not captured by dynamically inferred invariants, which may thus be unsound. Although this can be countered by producing additional executions with automated test generation techniques, it is crucial to generate new inputs that exercise relevant unobserved executions. In this talk I will present an ongoing work aiming to produce a test suite that, despite the limited set of executions, can automatically discover many sound invariants for Java classes.<\/p>\n <\/p>\n","protected":false},"excerpt":{"rendered":" The workshop will be held at\u00a0the Departamento de Computaci\u00f3n of the FCEyN (UBA) in room E-24 on 17 July. A preliminary schedule follows. Everyone interested is invited to participate! 10:00-10:15 Sergio Yovine and Eduardo Bonelli Opening remarks 10:15-10:50\u00a0Diego Figueira (CNRS,LaBRI, France) Logics for words and trees with data 10:50-11:25\u00a0Flavia Bonomo (UBA,CONICET) Three-colouring graphs without triangles … Continue reading Workshop INFINIS to be held on 17\/July\/2015 — Preliminary Programme — 20\/June\/2015<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-726","post","type-post","status-publish","format-standard","hentry","category-uncategorized"],"_links":{"self":[{"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=\/wp\/v2\/posts\/726","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=726"}],"version-history":[{"count":0,"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=\/wp\/v2\/posts\/726\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=726"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=726"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.irp-sinfin.org\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=726"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\nOpening remarks<\/span><\/p>\n
\nLogics for words and trees with data<\/span><\/p>\n
\nThree-colouring graphs without triangles or induced paths on seven vertices<\/span><\/p>\n
\nProjective quantum measurement in the lambda calculus<\/span><\/p>\n
\nInteractive Typed Tactic Programming in the Coq Proof Assistant<\/span><\/p>\n
\nMetrical versions of the Two Distances Theorem<\/span><\/p>\n
\nLow-level C code optimisations: are they valid?<\/span><\/p>\n
\nTowards An Evolutionary Approach to Unit-Level Invariant Discovery<\/span><\/p>\n
\n<\/strong>Closing remarks<\/span><\/p>\n————————————————————————————————————–
\nAbstracts of talks:<\/h2>\n
\nLogics for words and trees with data<\/span><\/p>\n
\nThree-colouring graphs without triangles or induced paths on seven vertices<\/span><\/p>\n
\nJoint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong<\/p>\n
\nProjective quantum measurement in the lambda calculus<\/span><\/p>\n
\nInteractive Typed Tactic Programming in the Coq Proof Assistant<\/span><\/p>\n
\nMetrical versions of the Two Distances Theorem<\/span><\/p>\n
\nLow-level C code optimisations: are they valid?<\/span><\/p>\n
\nTowards An Evolutionary Approach to Unit-Level Invariant Discovery<\/span><\/p>\n
\nOpening remarks<\/span><\/p>\n
\nLogics for words and trees with data<\/span><\/p>\n
\nThree-colouring graphs without triangles or induced paths on seven vertices<\/span><\/p>\n
\nProjective quantum measurement in the lambda calculus<\/span><\/p>\n
\nInteractive Typed Tactic Programming in the Coq Proof Assistant<\/span><\/p>\n
\nMetrical versions of the Two Distances Theorem<\/span><\/p>\n
\nLow-level C code optimisations: are they valid?<\/span><\/p>\n
\nTowards An Evolutionary Approach to Unit-Level Invariant Discovery<\/span><\/p>\n
\n<\/strong>Closing remarks<\/span><\/p>\n————————————————————————————————————–
\nAbstracts of talks:<\/h2>\n
\nLogics for words and trees with data<\/span><\/p>\n
\nThree-colouring graphs without triangles or induced paths on seven vertices<\/span><\/p>\n
\nJoint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong<\/p>\n
\nProjective quantum measurement in the lambda calculus<\/span><\/p>\n
\nInteractive Typed Tactic Programming in the Coq Proof Assistant<\/span><\/p>\n
\nMetrical versions of the Two Distances Theorem<\/span><\/p>\n
\nLow-level C code optimisations: are they valid?<\/span><\/p>\n
\nTowards An Evolutionary Approach to Unit-Level Invariant Discovery<\/span><\/p>\n
\nOpening remarks<\/span><\/p>\n
\nLogics for words and trees with data<\/span><\/p>\n
\nThree-colouring graphs without triangles or induced paths on seven vertices<\/span><\/p>\n
\nProjective quantum measurement in the lambda calculus<\/span><\/p>\n
\nInteractive Typed Tactic Programming in the Coq Proof Assistant<\/span><\/p>\n
\nMetrical versions of the Two Distances Theorem<\/span><\/p>\n
\nLow-level C code optimisations: are they valid?<\/span><\/p>\n
\nTowards An Evolutionary Approach to Unit-Level Invariant Discovery<\/span><\/p>\n
\n<\/strong>Closing remarks<\/span><\/p>\n————————————————————————————————————–
\nAbstracts of talks:<\/h2>\n
\nLogics for words and trees with data<\/span><\/p>\n
\nThree-colouring graphs without triangles or induced paths on seven vertices<\/span><\/p>\n
\nJoint work with M. Chudnovsky, P. Maceli, O. Schaudt, M. Stein and M. Zhong<\/p>\n
\nProjective quantum measurement in the lambda calculus<\/span><\/p>\n
\nInteractive Typed Tactic Programming in the Coq Proof Assistant<\/span><\/p>\n
\nMetrical versions of the Two Distances Theorem<\/span><\/p>\n
\nLow-level C code optimisations: are they valid?<\/span><\/p>\n
\nTowards An Evolutionary Approach to Unit-Level Invariant Discovery<\/span><\/p>\n