Il susțin pe Remus Cernea la prezidențiale

Eu îl susțin pe Remus Cernea la alegerile prezidențiale pentru ca nici unul din candidații partidelor politice nu mai au în ochii mei credibilitate. Pentru că m-am săturat de clasa politică românească, dar nu vreau să pierd speranța că se mai poate schimba ceva. Mă gândeam să nu mă duc la vot, până azi când am am aflat de Remus. E tânăr și nonconformist, îmi place cum gândește și îl admir pentru curaj. Nu a făcut politică, dar a fost implicat în societatea civilă. Nu are un partid puternic în spate (e candidatul Partidului Verde) și încă se chinuie să strângă cele 200.000 de semnături pentru candidatură, dar are idei interesante și duce un “război de gherilă” pentru atenția mass-media.

Mai multe informații găsiți pe situl oficial, sau într-un interviu pe metropotam.ro.

Even More Quotes

What the poet laments holds for the mathematician. That he writes his works with the blood of his heart. – Ludwig Boltzmann

“Bring forth what is true; Write it so it it’s clear. Defend it to your last breath.” – Ludwig Boltzmann, quoting Faust

“If there are no stupid questions, then what kind of questions do stupid people ask? Do they get smart just in time to ask questions?” – Scott Adams

To err is human, but to really screw up you need the root password.

A day without sunshine is like night. – Douglas Adams

Don’t start by thinking about a thesis or a thesis topic. Your goal is to produce papers. – Mihir Bellare about doing a PhD

Port Jefferson, NY

Intel Visual Computing Institute in Saarbrücken

Intel Corporation is investing $12 million to create a new research center that will explore advanced graphics and visual computing technologies. Opened May 12, the Intel Visual Computing Institute is located in Saarbrücken. The investment, to be made over 5 years, represents Intel’s largest European university collaboration.

• Intel Press Release
• Intel Blog: Announcing the Intel Visual Computing Institute (includes video)
• Presentation: Intel Visual Computing Institute – A New Hub in Europe for Worldwide Innovation (PDF 3MB)
• History of Collaboration between Saarland University and Intel (PDF 29KB)

Mobility of Young People in Europe (Questionnaire)

Young? Fond of traveling abroad to boost your education? What exactly do you expect to gain when studying abroad? Or when doing an internship abroad? Or when just doing a trip in some other country? Which advantages and disadvantages does a young person have when being mobile?

The Young European Federalists (JEF) want to study these questions and need your support. Their online questionnaire contains questions about mobility during education & training and requires approximately 10 minutes for filling in:

English Version/ German Version / French Version

Evaluation is anonymous and the results will be published after the 1st of August 2009 on the JEF website. JEF will use the results to make suggestions to politicians in order to achieve equal opportunities, to provide support and information for young people who want to travel abroad.

EU Profiler

Discover your position in the political landscape for the 2009 European Parliament Elections with the EU Profiler. Works for any EU country. All you need to do is to answer 30 general questions, and then you can compare how close your answer is to the official doctrine of the parties in the country you choose.

One thing that I still need to find out is the position of the different German parties on software patents. Does any of the readers have a clue?

The Saarbrücken Graduate School in Computer Science

• An integrated program from B.Sc. or M.Sc. to Ph.D.
• Study and conduct research at a top computer science location
• Stipends and other forms of financial support
• All courses are taught in English
• !!! Next application deadline: 30 April 2009 !!!
• More information at
  http://frweb.cs.uni-sb.de/index.php?id=7&L=0

List of Researchers now in Romania

Ad Astra has a list* of researchers based in Romania and their ISI publications between 2002 and 2006 (computer science). The data is not so recent** and seems to be quite noisy***, still the general image is quite clear. It could be useful if you want to do research in Romania and you are looking for an adviser or a university****.

* Because of unavoidable errors this is not a reliable ranking.

** More recent data seems to be available in Excel format only. The format is more raw though.

*** The site allows you to correct the information for your papers if you find anything wrong.

**** Such data was used to rank Romanian universities based on their research achievement, as I already wrote.

Beautiful Money

zk-typechecker 0.2.0 Released

The zero-knowledge type-checker is a tool for automatically analyzing the security of protocols that use zero-knowledge proofs. The analysis is modular and compositional, and provides security proofs for an unbounded number of protocol executions. The type-checker relies on the SPASS (or E) automated theorem prover to discharge proof obligations. It is released under the terms of the Apache License.

This release of the zero-knowledge type-checker adds support for security despite compromise and fixes many of the issues in the initial release (release notes). You can grab it from the page of the project.

Romanian Parliamentary Elections 2008

Duminica viitoare sunt alegerile parlamentare și m-am gândit sa postez mai multe informații importante mai ales pentru românii din diasporă.

• Situl MAE referitor la alegeri
• Coalitia România Curată: Listele Negre
• Ghidul alegătorului român din străinătate
• Secţiile de votare din străinătate
• Documente care atestă reşedinţa în străinătate

Typed Operational Reasoning

This semester I’m attending Derek’s course on Typed Operational Reasoning. Description from the site:

While many theorems about type systems are provable by straightforward induction, some properties are much trickier to prove and require a clever insight into how to “strengthen the induction hypothesis”. The method of logical relations provides such an insight, and it has been applied, generalized, and extended to prove a variety of interesting properties about typed programs. These include termination, strong normalization, decidability of type checking, consistency of type equivalence, contextual equivalence of programs, effectiveness of data abstraction mechanisms, and validity of program transformations. We will introduce the idea as it originated–Tait’s method for proving termination/strong normalization for the simply-typed lambda calculus–and eventually work our way up to equational reasoning about programs in a language supporting polymorphism, existential types, recursive functions, recursive types, and mutable references. Although the logical relations method is often used in the setting of denotational semantics, we will focus on how to use it to do operational reasoning about typed programs.

A secondary goal of the course is to convey a sense of how one actually does research and makes progress in programming language theory, or at least how I do it. Although classic results are often presented in the literature without any hint of their origins, in reality there is a continual, subtle interplay between the act of proving theorems and the act of discovering what theorems one wants to prove. (This is closely related to what Lakatos calls “the method of proofs and refutations”.) I will try to convey this interplay in the presentation of a number of topics in the course.

Washington

My First Students

Last week two of the students I supervise submitted their Bachelor’s Thesis. Both theses are about automatically generating executable code from abstract specifications of security protocols, however, the focus is quite different. While Alex worked on a very powerful tool that generates interoperable protocol implementations (to be released soon), Thorsten formalized a much simpler code generator and proved it to the preserve the security of the original protocol. In the future we would like of course to have both, the extensibility, flexibility and interoperability of Alex’ tool, with the same strong security guarantees as Thorsten proves for his generated code.

• Expi2Java – An Extensible Code Generator for Security Protocols (Alex Busenius)
  Abstract: This thesis presents expi2java, an extensible code generator for security protocols. We use a variant of Spi calculus for the protocol specifications and complement it with an expressive type system that is designed to reject inconsistent protocols. This type system features subtyping and parametric polymorphism. It is able to handle the types of nested terms, specialized channels and even low-level term configurations. Expi2java is highly customizable, easily extensible and generates interoperable Java code. We show the flexibility of our approach by generating an implementation of the Transport Layer Security (TLS) protocol.
• Spi2F# – A Prototype Code Generator for Security Protocols (Thorsten Tarrach)
  Abstract: This thesis describes a new prototype tool that automatically generates a secure F# implementation of any protocol described in the Spi calculus. Type systems were previously proposed for analysing the security of both Spi calculus processes and F# implementations. The thesis investigates a formal translation from the Spi calculus to F# that is proved to preserve typability, and therefore the security properties of the original protocol are preserved.

Life is Like a Jar of Rocks

A philosophy professor stood before his class and had some items in front of him. When the class began, wordlessly he picked up a very large and empty mayonnaise jar and proceeded to fill it with rocks, rocks about 2″ in diameter.

He then asked the students if the jar was full? They agreed that it was.

So the professor then picked up a box of pebbles and poured them into the jar. He shook the jar lightly. The pebbles, of course, rolled into the open areas between the rocks.

He then asked the students again if the jar was full. They agreed it was.

The professor picked up a box of sand and poured it into the jar. Of course, the sand filled up everything else.

He then asked once more if the jar was full. The students responded with an unanimous — yes.

The professor then produced two cans of beer from under the table and proceeded to pour their entire contents into the jar — effectively filling the empty space between the sand.

The students laughed. “Now,” said the professor, as the laughter subsided, “I want you to recognize that this jar represents your life. The rocks are the important things – your family, your spouse, your health, your children–things that if everything else was lost and only they remained, your life would still be full. The pebbles are the other things that matter like your job, your house, your car. The sand is everything else. The small stuff.”

“If you put the sand into the jar first,” he continued “there is no room for the pebbles or the rocks. The same goes for your life. If you spend all your time and energy on the small stuff, you will never have room for the things that are important to you. Pay attention to the things that are critical to your happiness. Play with your children. Take time to get medical checkups. Take your husband or wife out dancing. There will always be time to go to work, clean the house, give a dinner party and fix the disposal. “Take care of the rocks first — the things that really matter. Set your priorities. The rest is just sand.”

One of the students raised her hand and inquired what the beer represented.

The professor smiled. “I’m glad you asked. It just goes to show you that no matter how full your life may seem, there’s always room for a couple of beers.”