![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > Towards Algebra-Oriented Programming
![]() Towards Algebra-Oriented ProgrammingAdd to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other listsCERF Dr Chang Zhang Camtessential GroupOther talksSaving the People of the Forest: one chocolate bar and one nebulizer treatment at a time Intravital Imaging – Applications and Image Analysis/ Information session on Borysiewicz Biomedical Sciences Fellowships Art speak CANCELLED DUE TO STRIKE ACTION Recent advances in understanding climate, glacier and river dynamics in high mountain Asia Exploring the mechanisms of haematopoietic lineage progression at the single-cell level Breckland, birds and conservation |