Händelser: Data- och informationsteknikhttp://www.chalmers.se/sv/om-chalmers/kalendariumAktuella händelser på Chalmers tekniska högskolaFri, 25 Sep 2020 09:56:56 +0200http://www.chalmers.se/sv/om-chalmers/kalendariumhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Licentiate-Seminar-Victor-Lopez-Juan.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Licentiate-Seminar-Victor-Lopez-Juan.aspxVictor Lopez Juan, Computer Science and Engineering<p>Online</p><p>​Practical Unification for Dependent Type Checking</p><div><h3 class="chalmersElement-H3">Abstract</h3></div> <div>When using popular dependently-typed languages such as Agda, Idris or Coq to write a proof or a program, some function arguments can be omitted, both to decrease code size and to improve readability.  Type checking such a program involves inferring a combination of these implicit arguments that makes the program type-correct.<br /><br />Finding such a combination of implicit arguments entails solving a higher-order unification problem.<br />Because higher-order unification is undecidable, our aim is to infer the omitted arguments for as many programs as possible with a reasonable use of computational resources. The extent to which<br />these goals are achieved affect how usable a dependently-typed proof assistant or programming language is in practice.<br /><br />Current approaches to higher-order unification are in some cases too inflexible, postponing unification of terms until their types have been unified (Coq, Idris). In other cases they are too optimistic, which sometimes leads to ill-typed terms that break internal invariants (Agda).<br /><br />In order to increase the flexibility of our unifier without sacrificing soundness, we use the twin types technique by Gundry and McBride. We simplify their approach so that it can be used within an existing type<br />theory without changes to the syntax of terms. We also extend it so that it can handle more classes of constraints. We show that the resulting solutions are correct and unique.<br /><br />Finally, we implement the resulting unification algorithm on an existing type checker prototype for a smaller variant of the Agda language, developed by Mazzoli and Abel. We make a suitable choice of internal term representation, and use few, if any, example-specific optimizations. We obtain a type-checker which avoids ill-typed solutions, and is also able to handle some challenging examples in time and memory comparable to the existing Agda implementation. <br /></div>https://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Vetenskapsfestivalen-Algoritmer-som-påverkar-vår-vardag.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Vetenskapsfestivalen-Algoritmer-som-p%C3%A5verkar-v%C3%A5r-vardag.aspxDigitala Vetenskapsfestivalen: Algoritmer som påverkar vår vardag<p>Vetenskapsfestivalens digitala arena</p><p>​​IT-innovationer behövs för att skapa goda livsbetingelser för människan och samtidigt välfungerande ekosystem. Med IT kan vi effektivisera vår resursanvändning, fatta klokare beslut, stärka vår ekonomi och förbättra vår hälsa. Samtidigt behöver vi hantera hot som maktkoncentration, ekonomisk ojämlikhet, desinformation, övervakning och diskriminering. Den årliga Vetenskapsfestivalen har i år blivit flyttad från april till månadsskiftet september-oktober, och dessutom till en digital arena, som nås via vetenskapsfestivalen.se.</p> <h2 class="chalmersElement-H2">Program</h2> <p><strong>13.00 Medicinska beslutsstöd</strong><br />Mikael Elam, Sahlgrenska Akademin</p> <p><strong>13.15 Brottsbekämpning med textanalys</strong><br />Staffan Truvé, Recorded Future <br /></p> <p><strong>13.30 AI och kampen mot fattigdom</strong><br />Adel Daoud, Göteborgs universitet<br /></p> <p><strong>13.45 Paus</strong></p> <p><strong>13.55 AI och autonoma fordon</strong><br />Mats Nordlund, Zenuity</p> <p><strong>14.10 Ensuring privacy (på engelska)  </strong><br />Elisabet Lobo-Vesga, Chalmers</p> <p><strong>14.25 Nya möjligheter med kvantdatorer</strong><br />Marika Svensson, Chalmers</p> <p><strong>14.40 Paus </strong></p> <p><strong>14.50 Språkinlärning genom interaktion</strong><br />Emil Carlsson, Chalmers </p> <p><strong>15.05 Algoritmer som beslutsstöd</strong><br />Fredrik Johansson, Chalmers </p> <p><strong>15.20-15.40 Diskussion med frågor från publiken</strong><br /><strong></strong>Moderatorer under diskussionen är Claes Strannegård och Devdatt Dubhashi, Chalmers.<br /><br /></p>https://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Thesis-Defence-Charalampos-Stylianopoulos.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Thesis-Defence-Charalampos-Stylianopoulos.aspxCharalampos Stylianopoulos, Data- och informationsteknik<p>Zoom, link above</p><p>Hardware-Aware Algorithm Designs for Efficient Parallel and Distributed Processing</p> <p><br /></p> <p>The introduction and widespread adoption of the Internet of Things, together with emerging new industrial applications, bring new requirements in data processing. Specifically, the need for timely processing of data that arrives at high rates creates a challenge for the traditional cloud computing paradigm, where data collected at various sources is sent to the cloud for processing. As an approach to this challenge, processing algorithms and infrastructure are distributed from the cloud to multiple tiers of computing, closer to the sources of data. This creates a wide range of devices for algorithms to be deployed on and software designs to adapt to.</p> <p><br /></p> <p>In this thesis, we investigate how hardware-aware algorithm designs on a variety of platforms lead to algorithm implementations that efficiently utilize the underlying resources. We design, implement and evaluate new techniques for representative applications that involve the whole spectrum of devices, from resource-constrained sensors in the field, to highly parallel servers. At each tier of processing capability, we identify key architectural features that are relevant for applications and propose designs that make use of these features to achieve high-rate, timely and energy-efficient processing.</p> <p><br /></p> <p>In the first part of the thesis, we focus on high-end servers and utilize two main approaches to achieve high throughput processing: vectorization and thread parallelism. We employ vectorization for the case of pattern matching algorithms used in security applications. We show that re-thinking the design of algorithms to better utilize the resources available in the platforms they are deployed on, such as vector processing units, can bring significant speedups in processing throughout. We then show how thread-aware data distribution and proper inter-thread synchronization allow scalability, especially for the problem of high-rate network traffic monitoring. We design a parallelization scheme for sketch-based algorithms that summarize traffic information, which allows them to handle incoming data at high rates and be able to answer queries on that data efficiently, without overheads.</p> <p><br /></p> <p>In the second part of the thesis, we target the intermediate tier of computing devices and focus on the typical examples of hardware that is found there. We show how single-board computers with embedded accelerators can be used to handle the computationally heavy part of applications and showcase it specifically for pattern matching for security-related processing. We further identify key hardware features that affect the performance of pattern matching algorithms on such devices, present a co-evaluation framework to compare algorithms, and design a new algorithm that efficiently utilizes the hardware features.</p> <p><br /></p> <p>In the last part of the thesis, we shift the focus to the low-power, resource-constrained tier of processing devices. We target wireless sensor networks and study distributed data processing algorithms where the processing happens on the same devices that generate the data. Specifically, we focus on a continuous monitoring algorithm (geometric monitoring) that aims to minimize communication between nodes. By deploying that algorithm in action, under realistic environments, we demonstrate that the interplay between the network protocol and the application plays an important role in this layer of devices. Based on that observation, we co-design a continuous monitoring application with a modern network stack and augment it further with an in-network aggregation technique. In this way, we show that awareness of the underlying network stack is important to realize the full potential of the continuous monitoring algorithm.</p> <p><br /></p> <p>The techniques and solutions presented in this thesis contribute to better utilization of hardware characteristics, across a wide spectrum of platforms. We employ these techniques on problems that are representative examples of current and upcoming applications and contribute with an outlook of emerging possibilities that can build on the results of the thesis. </p>https://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Licentiate-Seminar-Bastian-Havers-Zulka.aspxhttps://www.chalmers.se/sv/institutioner/cse/kalendarium/Sidor/Licentiate-Seminar-Bastian-Havers-Zulka.aspxBastian Havers-Zulka, Data- och informationsteknik.<p>Online</p><p>​Distributed and Communication-Efficient Continuous Data Processing in Vehicular Cyber-Physical Systems</p>