Science

Ling - High level system programming

modular and precise resource management
Hall 6
Nicolas Pouillard
In this presentation I will present the experimental language Ling. We shall get an intuitive understanding of the language through familiar concepts from imperative programming. We shall cover how Ling enables a modular and precise control on memory allocation, through a general optimization called fusion. This optimization, fusion is a cost-free abstraction mechanism which brings high level programming to system programming.
The design of Ling is the result of my researches in collaboration with Daniel Gustafsson and Nicolas Guenot at the IT-University of Copenhagen and also from the language Limestone by Jean-Philippe Bernardy and Víctor López Juan at the University of Chalmers. These two lines of research stand upon the longstanding research topics of process calculi (such as the π-calculus), term calculi (such as λ-calculus), Linear Logic, and dependent Type Theory (such as used in Coq and Agda to write proofs and programs). The research on the λ-calculus and Type Theory gave rise to a powerful family of languages including but not limited to: Haskell, OCaml, Coq, Idris, and Agda. The research on the π-calculus gave rise to a vast family of calculi for concurrency. However type systems for these languages took much longer to emerge and progress. For instance the main concurrent programming language in use today is still dynamically typed. This is changing as we understand better how to the use the formulae of Linear Logic as behavior types (or session types) for concurrent processes. Still the aim of this experimental language is to program systems precisely and modularly. The need for precision comes from the resource constraints such as memory, file handles and the need for modularity comes the desire to reduce programming mistakes by solving problems at the right abstraction level. Functional programming offers a pretty good framework for modularity. This modularity comes at a cost which is rather difficult to predict. One the one hand optimizing compilers can fuse function composition to eliminate the need for intermediate data-structures. One the other hand when such an optimization fails to trigger the resulting program might poorly perform. The system of Ling controls when fusion can happen. Therefore one knows statically when fusion occurs and when intermediate buffers are needed. Today concurrent systems are built out of shared memory. However, the shared memory model is a nightmare for programmers. Here the approach is reversed we start from a concurrent programming language and apply it also for shared memory. At first the goal is not necessarily to target a parallel architecture but to program at level of abstraction where the programmer knows precisely the resources needed and the compiler still has plenty of opportunity to re-order and parallelize safely some instructions. This talk is intended at an audience familiar with imperative programming. Using the language should not require to understand anything about Linear Logic even though it is used fundamentally. Finally this presentation is an open call for comments and contributions to the open development of the language and infrastructure.

Additional information

Type lecture
Language English

More sessions

12/27/15
Science
greenstadt
Hall 2
What does the fact that Tor users can’t edit wikipedia mean for the quality of the ``encyclopedia that anyone can edit?’’ How do captchas and blocking of anonymity services affect the experiences of Tor users when they are trying to contribute content? This talk will discuss the increasing limitations of active participation in the anonymous Internet and the findings of our interview study of Tor users and wikipedia editors concerning these issues. We believe that by understanding the ...
12/27/15
Science
Hall 6
The REXUS/BEXUS programme allows students from universities and higher education colleges across Europe to carry out scientific and technological experiments on research rockets and balloons. Each year, two rockets and two balloons are launched, carrying up to 20 experiments designed and built by student teams. By reference of two experiments we were involved in, we will explain the way from the experiment idea to the launch and test of it.
12/27/15
Science
Philipp Winter
Hall 1
Several years ago, the Great Firewall of China was silently upgraded to find and block circumvention servers that employ encryption to defeat deep packet inspection. The system is now used to block protocols such as Tor, SoftEther, and SSH. In this talk, we will give an overview of how this system works, and how it can be circumvented.
12/27/15
Science
Peter Buschkamp
Hall 6
Light of astronomical objects gets distorted as it passes earth’s atmosphere. Adaptive optics can correct this distortion and create images that are as sharp as those taken in space. The correction needs a bright reference star. If there is no such star nearby, an artificial Laser Guide Star can be created in the upper atmosphere.
12/28/15
Science
Julia Maria Mönig
Hall G
In my talk I am 1) discussing philosophical concepts of privacy, especially Hannah Arendt's philosophy. I am 2) explaining why in a liberal-democratic system we need to protect our privacy and 3) what we can morally do to prevent catastrophes such as a totalitarian system from happening again. With Hannah Arendt's arguments and her analysis of totalitarian systems in mind, I am referring to three examples from today's privacy discussions: cybermobbing, Behavioral Advertising and secret services.
12/28/15
Science
Cornelius Diekmann
Hall G
We develop a tool to verify Linux netfilter/iptables firewalls rulesets. Then, we verify the verification tool itself. Warning: involves math! This talk is also an introduction to interactive theorem proving and programming in Isabelle/HOL. We strongly suggest that audience members have some familiarity with functional programming. A strong mathematical background is NOT required. TL;DR: Math is cool again, we now have the tools for "executable math". Also: iptables!
12/28/15
Science
Christian Schaffner
Hall 2
I will entertain the audience with a science talk about quantum cryptography, covering both some classics (Quantum Key Distribution) and the latest developments (position-based quantum cryptography) in this fascinating research field. [No previous knowledge of quantum mechanics is required to follow the talk.]