{"id":170943,"date":"2012-04-13T08:38:42","date_gmt":"2012-04-13T08:38:42","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/"},"modified":"2021-06-18T11:46:37","modified_gmt":"2021-06-18T18:46:37","slug":"koka","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/koka\/","title":{"rendered":"Koka"},"content":{"rendered":"<p class=\"asset-content\"><img loading=\"lazy\" decoding=\"async\" class=\"alignright\" src=\"https:\/\/avatars.githubusercontent.com\/u\/24441365?s=200&v=4\" alt=\"\" width=\"200\" height=\"200\" \/><\/p>\n<p>Koka is a strongly typed functional-style language with effect types and handlers.<\/p>\n<ul>\n<li>The core of Koka consists of a small set of well-studied language features, like first-class functions, a polymorphic type- and effect system, algebraic data types, and effect handlers. Each of these is composable and avoid the addition of \u201cspecial\u201d extensions by being as general as possible.<\/li>\n<li>Koka tracks the (side) <em>effects<\/em> of every function in its type, where pure and effectful computations are distinguished. The precise effect typing gives Koka <em>rock-solid semantics<\/em> backed by well-studied category theory, which makes Koka particularly easy to reason about for both humans and compilers.<\/li>\n<li><em>Effect handlers<\/em> let you define advanced control abstractions, like exceptions, async\/await, or probabilistic programs, as a user library in a typed and composable way.<\/li>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/koka-lang.github.io\/koka\/doc\/book.html#why-perceus\" rel=\"nofollow\">Perceus<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> is an advanced compilation method for reference counting. Together with <a href=\"https:\/\/www.microsoft.com\/en-us\/research\/publication\/generalized-evidence-passing-for-effect-handlers\/\">evidence translation<span class=\"sr-only\"> (opens in new tab)<\/span><\/a>, this lets Koka compile directly to C code <em>without needing a garbage collector or runtime system<\/em>. Perceus also performs <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/koka-lang.github.io\/koka\/doc\/book.html#why-fbip\" rel=\"nofollow\">reuse analysis<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> and optimizes functional-style programs to use in-place updates when possible.<\/li>\n<\/ul>\n<p>For more information, see:<\/p>\n<ul>\n<li><a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/koka-lang.github.io\/koka\/doc\/book.html#why\" rel=\"nofollow\">Why Koka?<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<li>The <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/koka-lang.github.io\/koka\/doc\/book.html\" rel=\"nofollow\">Koka book<span class=\"sr-only\"> (opens in new tab)<\/span><\/a> for a tour of the Koka language and its specification.<\/li>\n<li>Browse the repository at <a class=\"msr-external-link glyph-append glyph-append-open-in-new-tab glyph-append-xsmall\" href=\"https:\/\/github.com\/koka-lang\/koka\">github.com\/koka-lang\/koka<span class=\"sr-only\"> (opens in new tab)<\/span><\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Koka is a strongly typed functional-style language with effect types and handlers.<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13560],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-170943","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"2012-04-13","related-publications":[798427,1039398,860862,1041069,860991,1085355,671025,939696,165455,671076,953625,166405,671754,953640,277953,707329,953652,337556,731026,955017,387443,746071,965088,751681,982593,769738,1039380],"related-downloads":[755677],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Daan Leijen","user_id":31497,"people_section":"Section name 0","alias":"daan"}],"msr_research_lab":[199565],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170943"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":6,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170943\/revisions"}],"predecessor-version":[{"id":755689,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/170943\/revisions\/755689"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=170943"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=170943"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=170943"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=170943"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=170943"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}