Player is loading...
Taking Resources to the Type Level
Friday, June 14, 2019 · 11:48 a.m. · 35m 38s
With the Granule project, we are working towards making statically typed functional languages more resource-aware, hence providing a way to enforce stateful protocols regarding memory, file handles, network interaction, etc. Static enforcement of security policies and first-class support for multi-stage programming are further examples of what is possible in a type system based on Linear Logic and Graded Modalities. We present Granule, a functional programming language which combines parametric polymorphism and indexed types with such a type system. Granule programs will probably look very familiar to you, especially if you know some Haskell/ML, but in Granule’s type system we can reason about much more. Hillel Wayne’s Great Theorem Prover Showdown has made a point of the fact that there are many things we can’t easily reason about with functional (programming | proving)—up until now! We will implement leftPad in Granule and prove it correct with little more effort that writing the type signatures. We will then breeze through how Granule’s type system very naturally supports session-typed channels and safe mutable arrays.
Embed
Transcriptions
Note: this content has been automatically generated.
00:00:00
okay so um or maybe some of you disagree but
00:00:05
i think after all is very boring type system show
00:00:11
little information the types we can do so many things which we don't have to express the types so
00:00:17
um we're working on this thing called the granular language which is half the like uh looks a bit like hassle
00:00:23
it happens to be strict because that's um all vogue at the moment um but it is link yeah by default
00:00:31
and which is you know very painful like that pain of not being able to write many programs
00:00:38
well not quite like in high school you can make these programs we just have to make it explicit and and we'll see this
00:00:44
and we will learn about these fantastic graders modalities which i'm short about a hundred
00:00:49
years time i gonna be in scholar and maybe into energies time in the mainstream
00:00:56
okay so i'll to display must this is a
00:01:00
research language um we do have about thousand five hundred
00:01:04
commits ten thousand lines of code in like two hundred bits of stars which for academic thing is like
00:01:11
wow but i guess i'm uh you guys hit um
00:01:16
you weigh your and you wave repose with of uh and
00:01:20
units of measure i then asked the lonely academics and the um
00:01:27
we have very explicit so you can think of this absence of
00:01:30
cornstarch and to help us make very explicit what happens and programs
00:01:37
maybe we can maybe the the types gonna but nice to me there is some annoying things sometimes going
00:01:42
on all the time level which perhaps we can uh info uh and get some compiler to do for us
00:01:48
but at the moment that's not our focus so that's the display
00:01:54
what is the end of this talk that's not gonna greek in the stock
00:02:00
i hope if i actually if it in some rick somewhere i'm coming up so that um if you don't wanna
00:02:05
theatre wasn't tomatoes at me but if you don't wanna see it we have a nice if p. paper hopefully hopefully
00:02:12
because i'm gonna find out tonight whether actually got finally except we got a
00:02:15
conditional except on that um so it should be okay but we'll find out tonight
00:02:22
um so yeah everything in that paper and we will be getting a nice if each tutorial so if you're coming to i. c. p.
00:02:29
and you you like this you wanna see more of it then comes watches or oh
00:02:35
some motivations for linear it oh and i forgot to say what the
00:02:38
motivation of this talk was i said what it isn't so what is this
00:02:42
i just want to give you an overview of what granular does
00:02:44
hope to sort of um make you hungry formal um fancy type systems
00:02:52
and also maybe you guys can give me ideas on and how to actually make these things more practical so that would be fantastic as well
00:02:59
so what we millennium it we know about visions the things like in place up to eight
00:03:05
there's usage protocols file handles and these are actually we've gotten implemented and uh have a look at them in the second
00:03:12
um streaming audio session type channels which also implement it
00:03:17
um a lot a lot a lot lots of great reasons to have an i'm i'm currently playing around with um
00:03:24
having safe in interstate interface to a point is will references
00:03:29
um there's lots of fun stuff to explore our and and usable raise and so
00:03:36
that's also an aspect which i haven't had um many people talk about
00:03:39
which is program reasoning and we'll see a nice example fast as well
00:03:43
everything about optional code
00:03:49
so how well our land that our our and our um
00:03:54
what so so to speak is a base as the results so when you ask us for all
00:04:00
x. if x. infinitely copy ball is x. arbitrary
00:04:04
discoverable we will say i love philip what law now
00:04:08
okay so this is a quote from as the one what quote from a raise and hopefully new types contains about
00:04:17
um and that's the funny reason if you wanna know what he used the um upside down exclamation mark
00:04:22
to go on a paper that's for the plot have f. but what la luna types can change the well
00:04:29
um okay i handed if you're okay with that function no understand what that means
00:04:37
okay just to make sure everyone's and bought so the function that binds any value
00:04:43
type a we call it x. and it returns that value x.
00:04:49
okay great is this a linear function show of hands for uh for not
00:04:55
well some to maybe if i think yes it is a linear function okay
00:05:02
well i haven't told you will yet so this is a quite a trick question um and i'm just going to
00:05:07
uh get he was sort of intuition um in today's talk
00:05:11
and if you want to know exactly um the people um
00:05:16
but i think it's kind of easy to understand and some sense it
00:05:19
because it corresponds bit to how we reason about things in the real world
00:05:24
um so if you give me next i can give you thanks yet easy
00:05:29
um so this is what our interpreters that when we passed and this this exact function we can you
00:05:34
take the syntax exactly sort intern typewriter and it was like okay ah
00:05:42
this one here is that earlier have l. in the uh ram function i know i yes
00:05:51
okay and so okay so let's think about uh
00:05:54
what we did in i. d. yeah uh identity we
00:05:58
we um um we bound variable x. on the left and we were timed
00:06:04
it on the buttons so here on the left with binding a variable x.
00:06:08
i'm with binding their wine i and then we were turning why on the right hand side i'm returning x. on the right hand side
00:06:15
so we're giving back everything that we were given so that is like okay so our interpreters that's okay
00:06:26
what about this one copy if you give me any saying of type um
00:06:34
so this four o. eight actually qualifies of all types so if you give me anything in
00:06:39
the real world if you give it to me can i give you back two copies of it
00:06:43
no right so um as you might have guessed this is not a linear function
00:06:48
and our interpreter will stay in her to any verbal x. is used more than once
00:06:56
this year was also linear function
00:07:00
um when i when we you know especially painful linear you have to use it
00:07:05
okay which is which is great for for for for uh and um
00:07:10
weasels reasoning because we can then enforce things like something must be closed uh
00:07:15
you must free this memory exception okay so in the rubble axes never used
00:07:26
can actually implement anything in this well
00:07:31
let's let's play but with file handles
00:07:37
oops
00:07:40
okay
00:07:41
um
00:07:46
okay i'm not sure what the type that yet
00:07:54
uh oh okay let's open the file handle
00:08:00
open file
00:08:02
and
00:08:04
read mode
00:08:08
this is what i switched to this keyboard here um and now we
00:08:13
have to open the file gosh would be really nice and openness all's um
00:08:26
much uh uh
00:08:29
okay and what we get back from this is
00:08:36
uh_huh and um
00:08:40
this thing this this arrow is a bit um you know like
00:08:43
high schools by in a do notation which digit isn't to bind
00:08:48
um or ins gotta you have something i think for calm pretensions
00:08:54
i did my research
00:08:57
okay and then let's let's just let's say in
00:09:01
the forty two and it's good man type it
00:09:08
well uh open file is apparently one okay we keep changing things so let's have
00:09:13
a look inside where all the primitives of the fines and see what it's actually cool
00:09:19
oh it's called open handle now remember that the
00:09:26
oh
00:09:34
okay so alright sort of uh we have a problem here because this is
00:09:40
this is actually one adequate psychologist i can't just be doing effects that and um
00:09:48
and then returned a few but so
00:09:55
yeah
00:09:57
okay so actually this thing is we're not dick so let's say i
00:10:02
okay but now it's complain the neural h.'s never used that okay
00:10:08
so that use it um let's say i read file read handle
00:10:19
i
00:10:20
and then we get back a string
00:10:23
but not sticking to the permitted
00:10:28
um
00:10:32
what is the type of read handle uh in what was it called
00:10:37
is that we handle them
00:10:42
oh
00:10:44
open handle i'll okay read chop let's just read one correct
00:10:50
okay so if we do reach l. it gives us the take to handle
00:10:55
and it returns a character but it also returned the
00:10:59
new handle okay so a linear to basically forces us
00:11:09
uh but uh
00:11:13
okay this is this is kind of really hard to like uh like this looking backwards um and
00:11:18
most of my car uh talk was gonna be like reading but we still like it's it's um
00:11:27
and that gives us a
00:11:30
because i need a family cullen ooh that you can you explain it
00:11:37
okay
00:11:42
okay i i think i don't know i haven't done this one like that in ages i'd i hadn't planned to do this once and i think uh
00:11:48
it is reach out and i don't want to waste time and it's not
00:11:50
because of summarisation uh but yeah okay so that okay lets the quickly reach a
00:11:56
never mind that the things called stroll now okay so now
00:12:00
it's gonna complain again and and a fine and rose handle h.
00:12:11
and i lost i use my string okay well is it isn't my string well i'll just returned from now or
00:12:18
i could i could print and not return anything but that's just the towns uh it's actually chop okay um oops
00:12:32
yes yes
00:12:39
i'm sorry i'm i'm gonna have i don't know if i think if i could turn this thing around maybe
00:12:46
okay okay okay alright so what about what about copy we still can we still
00:12:51
don't have to copy okay well let's defined data types of brilliance data do all um
00:13:01
is that a good yet um now we want to the finder function that copies these buttons
00:13:11
um so we go from pool
00:13:16
to will crossbow and the cross is just me
00:13:21
just as the titans are prefer pets copy pool falls
00:13:28
was falls falls
00:13:35
and copied pool truer equals
00:13:40
true true a that works and this is not nonlinear because linear c.
00:13:47
is about variables usage of variables so so this thing here is actually okay
00:13:54
so does this mean you have to read lots of annoying wanna morphing functions now no
00:13:58
oh no no only country this is we don't like this one or more fake functions
00:14:02
because i called this copy balsam maybe you believe it copies but i
00:14:06
might be doing something sneaky like that's right and this would still type check
00:14:11
um so there we go we we do want home office and how can
00:14:16
we get our potable for them uh how can we get copy and polymorphism reconciled
00:14:23
back to the sledge okay
00:14:28
zero o'clock it doesn't work um so
00:14:33
so ensure us um originally new logic there is the type constructor called buying
00:14:39
i don't know if you go to the bank but everyone calls the back
00:14:42
um because it's an exclamation mark and everything in that bank can be used non linearly
00:14:51
so if we want to do copy we do a bang away to pass it right
00:14:56
and then added value level we given the parameter the for the the promise and copy is no
00:15:04
longer just of type a and type of is of type binary so there's a special let kind construct
00:15:10
um just to unwrap that that makes cents more or less
00:15:17
so think of these things are type constructors um and it's
00:15:22
just like say maybe something you need to just unwrap them okay
00:15:28
um no actually maybe is that's a high school thing is called options cousin
00:15:34
okay in glendale syntax this is what we did so we have these little boxes
00:15:40
behind a this means with with uh and a box of a or in a box
00:15:47
um and that the value level you do you use the brackets to to do it on boxing patent much
00:15:56
okay so we can do these two and then you'll and these things are actually sort of we use this um notation
00:16:03
because these correspond to two modalities from modal logic
00:16:08
um and we have the post topics which is very weird but they can get a
00:16:14
bit fall because there's actually these actually graded without so there's information studies were done to you
00:16:19
and once we write that in that they can get long so you know actually we still want to know
00:16:24
that the purpose of the type of the thing is still more interesting than modalities that we'd like to post
00:16:29
alright then down in the logic is basically think it
00:16:33
likely logic but it gives you more precise information says
00:16:37
um this function takes in a that is used at most twice
00:16:43
and drop takes in a that is used at most zero types
00:16:48
yeah so you get so you can know and the types distinguish between copy and drop
00:16:53
so the way this would look in glendale is like this
00:16:58
well good
00:17:01
any interjections any objections no okay alright so let's do demo and please please
00:17:08
ask we uh other questions during the demo and i get me to break things
00:17:15
um get lots of fun bugs exposed during talks it's the best
00:17:21
um okay
00:17:25
so that's the final data type for um optional is an okay i'll
00:17:34
is that the right yeah and then what would you call it non like that
00:17:39
okay good okay so what so in high school we have something called from maybe
00:17:46
what you call buttons colour which takes a the fault it hung
00:17:52
i guess or else okay okay i'm gonna call it from option okay um and
00:18:02
for all a we given a default value and we given an option okay
00:18:11
how we want to get back and okay yeah
00:18:15
from option in the file out and then in the non case we give back the defaults
00:18:24
uh and here we need to check so um uh
00:18:32
okay so let's say well maybe verbal accessories i made i made a mistake fine
00:18:40
oh no the available these never used ah alright so
00:18:44
we actually not using the default value in ten ten
00:18:50
okay okay let's breeze through this let's face or this um i promised to finish before lunch um
00:18:57
i will be the past the person holding out for lunch um okay so um i i i i'll be quick so
00:19:06
long story short reusing this a zero two wants yeah because that we can be super size
00:19:14
and now we still have to do all the time level unwrapping which is the thing i said to you is a bit
00:19:21
funky but necessary huh okay so now we're saying
00:19:27
we're using the default value zero two one times
00:19:31
and with the bug i did wanna copy and pasted the line where hans de here
00:19:37
which high school except at school it would accept this implementation and linear types hoppers for that
00:19:46
'cause we always gonna be linear in this option okay
00:19:51
alright so let's rooms rufus um lets him
00:19:56
import vectors
00:19:58
um have a quick look at
00:20:01
the oldest normal to find things i was going to define the myself actually but now um
00:20:08
due to time that says use the ones from the stand library so that just length indexed
00:20:13
so let's that i'll link the next of the type level yeah okay everyone loves them and i couldn't at least um
00:20:20
okay so now let's define the function left and
00:20:25
that that's
00:20:28
okay let's do like the hassle style it takes a char
00:20:32
which is of having character um or it takes desired length
00:20:40
and it takes
00:20:43
a list of child which is calls staples thing i think is back east
00:20:49
okay a vague idea what left hand does it takes a string and transits to add to a certain length
00:20:56
and given the timing character on the left yeah well good okay so
00:21:02
let's so so uh if you look at this type of this type is actually backpack type because
00:21:10
it's model think it's this implementation could depending on what sort of
00:21:15
having had to you giving it it could have completely different behaviour
00:21:19
okay so if you if you give it a space in my part of the left but then if
00:21:22
you pass it as as an asterisk it might have one right because it doesn't like plastic select and
00:21:29
so that's that's very that we want to be um if we want a reasonable could we want if we want to get the free spirit and
00:21:36
we need to be polymorphic okay that's fine we can do that and
00:21:40
ask we taken a instead of the ta and we go from lists of
00:21:48
that's what that's cool i'm sorry
00:21:52
okay
00:21:54
that's that's that and we can also do we can also um and shoulder lengths
00:21:59
of of of um of the input and output using type indices we can didn't have school
00:22:05
but how do we know that such a function doesn't always just give us
00:22:10
back a lot of having had to actually just throws away our original string
00:22:13
well with the new types we can actually guarantee that even a pure code
00:22:18
so we get nice guarantees so if we have a function
00:22:21
f. and a four will a and and and i it's okay
00:22:34
um we take a padding character
00:22:38
we take
00:22:41
this is uh this is just an index in singleton encoded natural
00:22:47
yeah we take 'em back and input string and we give back
00:22:52
and output string and we're going to say it's going to be the
00:23:01
max of and and
00:23:05
okay
00:23:06
well we'll be able to implement such a function foo okay why why can we not implement this function
00:23:15
yes so that a is it we're going to use a non then you so we what we're gonna do in here is something like
00:23:21
uh left high and having heard or and ah it's called x.
00:23:28
and x. the is is like
00:23:32
replicate and one with length of taxes
00:23:39
x. plus x. it's something like that yeah so i'm at what's your name
00:23:49
q. s. o. same as my name villain hume it's any different um
00:23:55
so as the only pointed out we're gonna have to use the x. here
00:24:00
non linearly so what is replicate has replicate implemented let's have a look that good okay
00:24:06
how we take a number and we take an array that has to be valuable that many times okay so we
00:24:14
he's right week we really can't implement that's like that okay but if we probably get the constraint that we need
00:24:21
that uh uh that we need that a um non linearly then then we're gonna be fine
00:24:27
but what are we gonna put in the how many times are we gonna be using the a
00:24:36
zero to em
00:24:39
hum
00:24:42
my notes say otherwise my notes that this and known as an right so n.
00:24:48
is the desired length and is the actual length so if the desired length um
00:24:56
is bigger than the than the actual length then we get that then we're gonna subtract the actual links and we get we
00:25:03
left over with the with the number of cutting elements we need okay and because this is known as we just cut off it
00:25:12
yep
00:25:15
uh no nuts so we just we ended up there
00:25:19
yeah a little cutoff subtraction some people call
00:25:25
okay
00:25:27
we still doing something bad idea actually which is a bit annoying because
00:25:31
it's actually not that we're using when using a the lists non linearly
00:25:38
i don't know how we gonna get around this well uh we need to do to come up on the thing
00:25:45
well we can say um we can get the length of the list
00:25:51
uh that an axes of length of x. x. is in
00:25:58
uh yeah um oh look at that we have to what lengths function that actually gives a list back
00:26:06
uh_huh
00:26:18
so when the no case we return zero and in the cons case we um
00:26:26
we require us on the in the list and then we build it back up yeah
00:26:32
yep this is sort of our constructive proof that this is really the length is
00:26:36
is is sort of lynn yeah that we can still have a list after taking slacks
00:26:45
um and become but that's about it like this um okay this should work
00:26:56
um length prime are what
00:27:04
i did last minute fiddling around with things which is always recommended
00:27:15
could not resolve upper timeliness
00:27:18
mm how right sure um this is actually the time level
00:27:23
things goldman is and is also defined in the next slide free
00:27:29
and um but um yeah i don't know whatever
00:27:35
what's it works and i don't have time to fix it now um does of the trials of
00:27:38
life today but we can sit down together and and break it more if you want after that
00:27:43
um so let's go right to a slight good talk about these lovely send earrings with
00:27:49
uh which martin overdue you told us about and what should we gonna have much in
00:27:58
that a free minutes
00:28:03
'kay quick overview gonna subsystem and with index types
00:28:07
in your single delta these blah blah blah marketing
00:28:10
um we use an s. m. t. cell that we use that three which hopefully discharges are constraints
00:28:16
but these things are sort of of uh things like natural number paula no males they're not um
00:28:22
not the slide and but they seem to work really well for for the things we've been considering so far
00:28:28
and and you don't have to do the clunky sort of manual and things
00:28:32
like an actor or a dress and which people hate i love them but
00:28:39
okay very very quickly we use you use these endearing
00:28:45
operations um like bound like d. from band of any logic
00:28:51
and which is uses normal natural number plus the multiplication actually with parametric over this anyway
00:28:58
so we can actually say well this is the row and this class they don't need to be natural gas
00:29:04
we might be we we might want to do all
00:29:06
the um analyses fact give different meetings to these things so
00:29:15
so there's things like billy there's the uh brilliance endearing which can give us an for
00:29:19
we can use to track information like well for example is it linear is it not linear
00:29:25
all is if your is it not your is it total is it possible
00:29:30
and the extended not roles allow us to to reason about things
00:29:36
when you add sort of infinity to the natural numbers and and
00:29:41
by you reach sort of a tall uh which is the top element which reach when you don't really don't know if you have no upper bound on the news
00:29:48
um and so on i've my should bring a bit of of of skeleton facts into this
00:29:54
slide and so we can have interval which is a very quickly on option we have to use um
00:30:00
we had to use the default zero two one times so that's into that we could take any send hearing
00:30:05
any preordained figuring and and do in and lifted an interval which is fan also it's anyway
00:30:12
so it's like a higher order blah blah blah and one oil um uh i kind of you can also plug in one it's where
00:30:19
you are uh use the zero and the one oppose the same element
00:30:23
ends the plus sometimes about the segment of the same operation and um
00:30:30
yes celebration so things like sets of labels and to
00:30:33
track affects and patterson plus it's this is something i'd
00:30:37
be interested about whether we can give 'em in bed and plus it's an offering like reason button in that way
00:30:46
and i think one just one um uh what i want to drop here
00:30:50
is um algebraic effect so there's a there's a very strong a correspondence and um
00:30:56
uh intimate relationship with algebraic effectiveness but gets to be explored fully
00:31:04
future work okay so very quickly edwin was so nice to visit our the us to
00:31:09
visit our departments and a few months ago and he showed us interest to an action
00:31:15
and he is found that the troops search which happens to be
00:31:19
time and fronts yeah so that is exciting also to industrial uh develop an um
00:31:26
gets much pets of linear types when you constrain the such space by saying
00:31:31
well i know that you should be using you you should be using this linearly
00:31:35
we should be using the sun was twice then we cut out a lot of bad programs and that helps
00:31:41
with inference and maybe yes we add a bit of the add a bit of extra things for the types
00:31:47
so in the case of left pad all we have to add to the sort of type
00:31:52
like the mildly interesting type in high school where you actually keep track of the correct lengths
00:31:57
um well we had to add was that one little m. understand
00:32:00
right but that cuts out on lots of bad implementations in fact
00:32:05
one of the bad implementations except the ones that don't put the padding correct and right place so it gives us a sort of
00:32:11
verification or lightweight verification on suns resource like properties
00:32:18
um no i think this is this i think this is cool subway too lax i i want to go much
00:32:24
farther i want to be more i would be more
00:32:27
constraining um we still have exchange which is another structural um
00:32:33
structure ruin type systems which classes use and turn level variables in any order
00:32:38
that's how we don't wanna use to from anywhere that's just messy i mean he wears
00:32:42
what's and i've you all can agree with me right has to be like what um
00:32:47
so let's say and and and i was thinking uh sitting at the train station uh
00:32:51
doing some the slides yesterday thinking well what i'm gonna call this modality what i'm gonna
00:32:55
a thought that lets you can eat things that maybe some service and you get the reference the very deeply and okay
00:33:03
so this is our normal that function and see we have to explain
00:33:08
that the f. commutes because the f. is used um both here in the
00:33:14
bush here and thirties personally neely hands
00:33:19
obviously whenever you something only need wow yeah it's it's not use in
00:33:23
an orderly fashion but like that so if what if someone gave you
00:33:27
wrote your give you the signature and you don't know that yet because
00:33:32
that was the slide builds um i thought like and what if um
00:33:38
and the something's in the what if someone gave you a mac function that actually switched all the elements around
00:33:45
that would still be okay with the normal in your type now if we feel is the biggest to
00:33:51
live to be must also be ordered then we know that this function can't just be switching when things
00:33:56
and my theory my theory is that maybe you don't need to be
00:33:59
switching and stuff behind people's backs so much maybe making this explicit it's
00:34:04
could also be interesting for at least proving properties maybe in library functions i'm sure you
00:34:10
wouldn't want to have to do that kind of stuff and become what we find um
00:34:14
but it's kind of a nice way uses lots of new three prepared this
00:34:18
hasn't really been formalised so this is something i want to i'm looking to irons
00:34:25
that's it i was gonna show you what a a remote code still but i think we've run out of time
00:34:30
so if you wanna see any of the point uh as um i did a few playing around
00:34:34
with and there is so there's lots of papers
00:34:37
in that area which which alex thirty pages long
00:34:41
and we're able to express them because we don't have to run your we don't have to explain all the
00:34:45
things around howling actually what we've got a framework for
00:34:48
free for regular board three and for playing rambling arty
00:34:53
so we can explain these ideas and a few lines of comes from which is really cool
00:35:06
okay thanks a lot we really were noble time here so we have one
00:35:09
minus two minutes left which i think really something of linear to constrain coming up
00:35:16
um he's view would be supine a him fold
00:35:20
you so you can go outside and just fold use
00:35:24
your whole someone else because they know where she is
Conference Program
Keynote: Some Mistakes We Made When Designing Implicits (And Some Things We Got Right)
Martin Odersky, Professor EPFL, Chairman Typesafe
June 14, 2019 · 9:13 a.m.
303 views
Brave New World - tales of PureScript and Haskell in production
Felix Mulder, Snoop Dogg
June 14, 2019 · 10:22 a.m.
151 views
Actors Design Patterns and Arrowised FRP
June 14, 2019 · 10:53 a.m.
Taking Resources to the Type Level
June 14, 2019 · 11:48 a.m.
Lord of the rings: the Spire numerical towers
Denis Rosset, researcher in quantum physics
June 14, 2019 · 1:47 p.m.
Formal verification of Scala programs with Stainless
June 14, 2019 · 2:20 p.m.
118 views
Exploring Scala Tooling ecosystem
Jeferson David Ossa, Colombia
June 14, 2019 · 3:12 p.m.
TwoFace values: a bridge between terms and types
June 14, 2019 · 3:43 p.m.
GADTs in Dotty
June 14, 2019 · 4:41 p.m.
302 views
Closing Remarks
June 14, 2019 · 5:49 p.m.
Recommended talks
Mellite: An Integrated Development Environment for Sound
Hanns Holger Rutz, Institute of Electronic Music and Acoustics (IEM), Graz
June 13, 2019 · 4:48 p.m.
213 views
Compiling to preserve our privacy
Manohar Jonnalagedda and Jakob Odersky, Inpher
June 13, 2019 · 12:17 p.m.
302 views