Tutorials

APLAS/CPP offers two free tutorials, on 4th December, to all registrants.

Tutorial 1: Dependently Typed Programming in Adga

  • Lecturer: Shin-Cheng Mu (Institute of Information Science, Academia Sinica)
  • Date: Sunday, 4th December 2011
  • Time: 9 am - 12:00 noon.

The type of a function specifies properties it is supposed to satisfy. Modern programming languages incorporate advanced type systems, thus more and more properties can be expressed and verified by the type checker.

While the dependent type is known to be one of the most expressive type systems around, it is not yet clear how to harness its power in a programming language. In recent years, it has been a popular topic to experiment with new programming language designs, aiming to bridge the gap between type theory and practical programming. Projects along this line include Cayenne, Epigram, Coq, Dependent ML/ATS, Omega, and Agda, etc.

In this short tutorial we will, through live demo, construct some interesting Agda programs, and see how dependent types help to ensure program correctness.

Most of the course material is courtesy of Conor McBride.

Course outline:

  • An Introduction to Agda and Dependent Types
  • Inductive Families
  • Example: a Verified Compiler
  • Generic Programming using Dependent Types
  • Datatype Differentiation, and the Zipper Structure
  • Datatype Ornamentation: from Nats, to Lists, to Vectors

Tutorial 2: Parallelizing Legacy Sequential Code

  • Lecturer: Lei Liu (Institute of Computing Technology, Chinese Academy of Sciences)
  • Date: Sunday, 4th Wednesday 7, December 2011
  • Time: 2 pm - 5 pm 3 pm - 6 pm.

With the advent of multi-core architecture, parallel processors are becoming prevalent and bring many programming challenges. A large amount of existent programs were designed for uni-processors, how to divide these legacy codes into tasks and execute them simultaneously on different cores with a small number of developers' effort, is a highly challenging work. As is well known, automatic parallelization technologies have been studied for decades, but current production and research compilers with this functionality available to the users often provide only moderate profit, or sometimes even degrade the performance. Furthermore, compilers without programmers' knowledge cannot provide optimal solutions for complex programs.

Therefore, we strive to improve this situation by two fold efforts. At the first place, we enhance the effectiveness of automatic parallelization via more powerful parallelism exploiting techniques and accurate scheduling strategies for locality in parallel setting. We are also focusing on user interaction based approaches that can help programmer to make smarter parallelizing decisions, and our parallel programming model can safeguard the correctness of parallelization to a certain extent.

Moreover, our parallel programming system provides tools that can analyze the runtime feedback and generate more optimized tuning advice for users, so as to support incremental parallelization. With a set of experimentations on practical applications, our methods have shown promising results. We are confident that our system can generate better parallelized code for Multi-core/Many-core platforms comparing to existing schemes.

 
tutorials.txt · Last modified: 2011/12/02 17:56 by trc     Back to top
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by LouisWolf