Towards Algebra-Oriented Programming

Add to your list(s) Download to your calendar using vCal

• Bruno Oliveira, National University of Singapore
• Tuesday 02 April 2013, 10:00-11:00
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

This event may be recorded and made available internally or externally via http://research.microsoft.com. Microsoft will own the copyright of any recordings made. If you do not wish to have your image/voice recorded please consider this before attending

Programs can be modularly decomposed in several dimensions. However, it has long been noted that existing programming languages typically suffer from ``the tyranny of the dominant decomposition’’, only supporting decomposition of programs well in one dimension. Bad support for other dimensions leads to crosscutting concerns: code that logically represents some separate, modular functionality of the program, but which is not easily modularized. The main problem lies in existing programming language structuring abstractions, such as algebraic/inductive datatypes in functional languages or object interfaces in object-oriented languages, which dictate the particular flavor of modularity supported by the language.

This talk suggests a form of algebraic signatures, which we generally refer to as algebras, as an alternative programming language structuring abstraction. Algebras do not dictate a particular modularity dimension on the programmer. Instead they support various composition operators which allow them to cater for several dimensions of modularity at once. Algebras have desirable properties of a programming abstraction: they support modular type-checking, separate-compilation and modular reasoning/proofs. I will show how algebras can already be encoded in existing programming languages and theorem provers, and how they can help dealing with several practical problems: from modularizing DSL components, to modularizing inductive proofs and meta-theory of programming languages. I’ll finish the talk by discussing some of the remaining challenges on creating truly algebra-oriented programming languages.

This talk is part of the Microsoft Research Cambridge, public talks series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Auditorium, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• personal list
• rp587

Note that ex-directory lists are not shown.