Index of /private_videos_57fjf23FdKspj

	Name	Last modified	Size	Description
	Parent Directory		-
	README.html	2016-07-06 15:49	12K
	biosense.mp4	2016-06-29 18:13	5.9G
	biosense_compressed.mp4	2016-07-06 14:41	279M
	creating_bachelor_course_in_english_in_serbia_compressed.mp4	2016-07-06 15:37	158M
	drytools_compressed.mp4	2016-07-06 14:32	201M
	dsl_hpc_compressed.mp4	2016-07-05 17:55	176M
	epfl_novi-sad_scopes_meeting.html	2016-07-06 15:49	12K
	heather_miller-scala_compressed.mp4	2016-07-01 11:51	176M
	implicit_web_builder_dupriez_compressed.mp4	2016-07-06 11:26	119M
	modular_semi-automated_printing_mayer_compressed.mp4	2016-07-06 11:26	180M
	nada_amin_LMS_compressed.mp4	2016-06-30 15:40	498M
	proving_performance_properties_ravi_compressed.mp4	2016-07-06 14:32	288M
	scala_native_denys_compressed.mp4	2016-07-06 10:21	326M
	scopes_compressed.mp4	2016-07-05 17:58	279M
	viktor_kuncak_introduction_compressed.mp4	2016-07-01 10:21	139M

EPFL - Novi Sad SCOPES Meeting
Wednesday 29 June 2016 08:45 - 17:00 BC420

Program

08:45 Welcome coffee and croissants served in front of BC 420
09:15 Viktor Kuncak: Introduction
09:30 Nada Amin: LMS: Generative Programming in Scala
10:30 Srdjan Škrbić: SCOPES project Research and Education Goals and Results
11:00 Dragan Mašulović: Creating a bachelor CS course in English in Serbia
11:30 Vladimir Crnojević: Presentation of the BioSense center, Novi Sad

12:00 Lunch (15 people)

13:45 Heather Klug: Scala Center
14:00 Sergi Mateo Bellido: Domain Specific Languages on HPC systems
14:30 Denys Shabalin: Scala Native
15:00 Marko Gaćeša and Nikola Milinković: Drytools

15:30 Coffee break

16:00 Mikaël Mayer and Thomas Dupriez: Modular synthesis of serializers from examples
16:30 Ravichandhran Kandhadai Madhavan: Proving performance properties
17:00 End of the presentations

Abstracts of talks

Nada Amin: LMS: Generative Programming in Scala
Lightweight Modular Staging (LMS) is a Scala library for generative programming: the key idea is to write high-level generic programs that generate low-level specialized programs at runtime. The LMS framework provides a library of core components for building expressive embedded DSLs, as well as high performance code generators and compilers. We will see several examples, including a SQL to C compiler that performs advanced data layout optimizations and is written in less than 500 lines of code.
Along the way, we will discuss concepts such as mixed-stage data structures that contain both static and dynamic parts (e.g. static schema and dynamic values for data records) and staged interpreters which can be mechanically turned into compilers (e.g. for SQL queries or regular expressions). Finally, we will touch upon ongoing work for verifying properties (e.g. no memory nor overflow errors, checked contracts) of the low-level generated code, so that it is not only fast but also secure.

Srdjan Skrbic: SCOPES project Research and Education Goals and Results
In this talk I will give details about research activities foreseen within the SCOPES IZ74Z0_160453 project, as well as goals associated with building educational capacities. Progress related to each activity will be presented and discussed.

Dragan Mašulović : Creating a bachelor CS course in English in Serbia
In this talk we would like to discuss challenges of creating and implementing an English CS course in a non-english speaking country such as Serbia. We would appreciate feedback from our EPFL colleagues who have rich experience in implementing such courses on all levels of academic education.

Vladimir Crnojević : BioSense Institute - Data in Action
Research and Development Institute for Information Technologies in Bio- systems, also known as the BioSense Institute, has been founded to focus multidisciplinary, game-changing and needs-driven research and disseminate it to a global ecosystem of forward-looking stakeholders. Multidisciplinary research is performed in the fields of micro and nanoelectronics, communications, signal processing, remote sensing, big data, robotics and biosystems, with a common goal to cross-fertilize various bio-fields with ICT. BioSense promotes data science in various traditional bio-systems by solving different problems, difficult to comprehend with traditional knowledge – smart choice of seeds in agriculture, clustering of gene sequences, AIDS breakout modeling through mobile subscribers behavior etc. Putting the data in action to make the real benefit for biosystems- the real mission of BioSense Institute.

Sergi Mateo Bellido: Domain Specific Languages on HPC systems
The talk will present our experiences developing a framework to build Domain Specific Languages for HPC platforms. This multi-layer framework is based on LMS for embedding DSLs and OpenMP and MPI for running on parallel and distributed environments. Our framework has been successfully used to implement a DSL for solving problems that can be modeled as a set of Partial Differential Equations (PDEs). This specific DSL will be used to describe our software architecture and the different challenges and opportunities we identified to effectively develop DSLs for HPC systems.

Denys Shabalin: From Scala to native with Scala Native
Scala has historically been a JVM-centric programming language. The situation has started to change with appearance of the Scala.js that opened a door of front-end development to Scala programmers. With Scala Native we're expanding the horizons of Scala applications even further via ahead-of-time compilation to native code through LLVM. This talk is going to walk you through all the transformations that happen starting from the high-level Scala code and ending with the target machine code.

Marko Gaćeša and Nikola Milinković: Application of DSLs in modelling higher level abstractions of client/server systems
Programming is still too slow and expensive, mainly because a lot of code has to be written, integrated and tested even when the concepts and the solution are clear. Applying domain specific modelling helps but the real challenge lies in finding an optimal balance of concepts that are common enough and high level enough to be specified in the DSL vs a GPL. We explore the problem on a concrete example of a DSL that describes cloud based client/server systems.

Mikaël Mayer and Thomas Dupriez: Modular synthesis of serializers from examples
Printing, or serializing a tree to an exportable string representation, such as CSV, XML, HTML, JSON, is a task often involving several serialization functions calling each other, possibly recursively. We present a novel way to interactively synthesize such printers through input/output examples. To reduce the time the user takes to write examples, after each example - and even before any example is entered - we provide the user coherent alternatives of rendering a new input if they exist. The user may edit the output before choosing it. In addition, we support the synthesis of generic printers with abstract printers in their arguments, with the same interaction mode. It gives the freedom for the user to synthesize printers bottom-up or top-down or in any other order. Our framework is totally integrated into the online vérifier and synthesizer Leon. The user has thus full control on the way examples are added and removed by editing them in the code.

Ravichandhran Madhavan: Proving Performance Properties of Higher-order Functions with Memoization
Static estimation of performance properties of programs is an important problem that has attracted great deal of research. However, most existing tools automatically infer best-effort upper bounds, and hope that they match users expectations. In this talk, I will introduce a system “Orb” that supports verifying symbolic user-specified bounds on resources such as evaluation steps, and stack space, akin to a verifier for correctness properties. Our approach is targeted at functional programs with first class functions that may use lazy evaluation and/or memoization. In our approach, users could specify the desired resource bound as a template with numerical holes e.g. as  time <= ? ∗ size(l) + ? , along with other functional properties necessary for establishing the bounds. We developed an algorithm for verifying the bounds by automatically inferring values for the holes, while accounting for the effects of memoization, and lazy evaluation. In addition, our approach can also disprove concrete bounds by finding counter-examples. Using our tool Orb, we verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions, and memoization. The benchmarks include Okasaki’s real-time queues, deques, lazy data structures based on numerical representations such as lazy binomial heaps, catenable queues, cyclic streams, and dynamic programming algorithms like weighted scheduling, and packrat parsing, which have posed serious challenges to automatic as well as manual reasoning.

Contact Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch

Accessibility Informed public