News

Subsidie voor fundamenteel informatica onderzoek aan Lambda calculus.

Een NWO subsidie van EUR 200.000 is toegekend aan het onderzoeksproject "Clock Semantics for Lambda Calculus". Professor Jan Willem Klop en Dr Femke van Raamsdonk zijn beide docenten en onderzoekers aan de VU, bij de Theoretische Informatica onderzoeksgroep. Ze gaan de komende 3 jaar onderzoek doen naar de eigenschappen van deze "Clock Semantics"

Lambda Calculus, een formeel systeem dat rekent met lambda termen als elementaire informatiedragers, vormt het hart van diverse functionele programmeertalen alsmede van de theorie van berekenbaarheid waarop de informatica is gegrondvest. De semantiek van deze oerprogrammeertaal  bepaalt hoe scherp haar 'onderscheidend vermogen' is, zoals een optisch instrument dat ook heeft.

In ons project realiseren we een essentiele verscherping waardoor uiteindelijk de toepasbaarheid  verhoogd wordt in het  bewijzen van correctheid van software, en  daaruit voortvloeiend,  veiligheid en betrouwbaarheid van complexe systemen. Deze verfijnde semantiek bereiken we door onze recente ontdekking  en benutting van een inherent klokmechanisme dat zich manifesteert in de werking van lambda termen.

Onze bijzondere interesse gaat daarbij uit naar 'fixed point combinators', die het fundamentele principe van recursie herbergen.

___________________________________________

[English translation]

Grant for fundamental computer science research on the field of Lambda calculus

An NWO grant of EUR 200.000 has been awarded for the researchproject "Clock Semantics for Lambda Calculus". Professor Jan Willem Klop and Dr Femke van Raamsdonk are both teachers and researchers at the Theoretical Computer Science group of the VU University, They will do research for the next three years on the properties of these "Clock Semantics"

Lambda Calculus is a formal system computing with lambda terms as elementary carriers of information. It constitutes the heart of various  functional programming languages, as well as the theory of computation on which computer science is founded. The semantics of this 'ur-programming language' determines the sharpness of the discrimination power, much like optical intruments possess.

In our project we realize an essential increase of this sharpness, eventually aiming to progress in proving correctness of sotware and the ensuing safety and security of complex information systems. We reach this refined semantics through our recent discovery and exploitation of an inherent clock mechanism, present in the evaluation of lambda terms.

In particular we study in this sharper semantics the working of 'fixed point combinators', embodying the very principle of recursion.