This year, the students are organizing a series of talks on things that we find interesting. This can be anything from subtle mathematical points that supplement the lectures to completed research results to descriptions of ongoing projects. It's a good chance to meet others who are working on similar projects or who have similar interests as well as a good way to practice upcoming talks and to get better at communication.
There will be two categories of talks: twenty-minute talks and five-minute talks. If you would like to hold a talk, please email David at drc at itu dot dk or reply to the mailing list post. So far, we have reserved the colloquium room in Deschutes on Friday, July 26 and Tuesday, July 30. It is possible to arrange another evening if the student talks prove to be even more popular than expected.
Time limits will be strictly enforced to make sure that everyone gets a chance. If you need a different amount of time than either 20 or 5 minutes, then we can set something up. There will be time for questions after every talk.
Please be at Deschutes Hall at the starting time promptly. The lecture hall is on the floor above ground level, so we may not be able to let you in late.
8:10 - 8:30 | Leah | Julia is a high-level, high-performance dynamic programming language for technical computing, with syntax that is familiar to users of other technical computing environments. |
8:40 - 9:00 | David Thibodeau | Copatterns are a means of programming with potentially infinite data structures focused around observations rather than destructuring. |
9:10 - 9:15 | Lindsey Kuper | LVars, laconically |
9:20 - 9:25 | Peng Wang | Compositional Compiler Verification via a Program Logic |
9:30 - 9:50 | Jason Gross | The basic topological intuition and terminology for homotopy type theory. This is a talk on "this is a space, this is a path, this is a homotopy, this is what discrete means, this is what contractible means, etc" that I've given informally to a few friends in the past. |
9:50-10:00 | Clean up | The lecture hall is used for doctoral defenses and other events during the day, so I've promised to leave it as least as clean and orderly as we find it. |
The talks tonight start 30 minutes earlier, to make space for the high level of interest. Please be at Deschutes no later than 7:30 PM.
n7:40 - 8:00 | Mounir Assaf | Non-Interference Verification |
8:10 - 8:30 | David Christiansen | Type Providers in Idris |
8:40 - 9:00 | David Thibodeau | Beluga |
9:10 - 9:30 | Álvaro García Pérez | Proving Correctness of Interpreters for the Gradually Typed Lambda Calculus |
9:40 - 10:00 | Jason Gross | Basic Category Theory |
10:00 - 10:10 | Clean up | The lecture hall is used for doctoral defenses and other events during the day, so I've promised to leave it as least as clean and orderly as we find it. |
7:40 - 8:00 | Reed Morgan Milewicz | I would like to talk about my work on extending the C++ language to support concepts (constraints on generic types) on Tuesday for 20 minutes. Despite the subject matter, I promise that it will be an entertaining and exciting journey. I am especially interested in receiving feedback, criticism, and questions, seeing as I'll be presenting my work at a conference in September. |
8:10 - 8:15 | Piotr Mardziel | Probabilistic Computation and Information Security |
8:20 - 8:25 | Robert Rand | Probability Theory and Hoare Logic |
8:30 - 8:35 | Yuting Wang | The Abella theorem prover |
8:40 - 9:00 | Abhishek Anand | Type Theory of Nuprl. I would describe Nuprl's type theory and compare it with the HoTT/Coq/Agda. The key difference is that Nuprl has curry syle typing(terms are not annotated with types) and equality is extensional. I will also explain the quotient, intersection and partial types of Nuprl and their usefulness in expressing various properties about programs and mathematical objects. |
9:10 - 9:30 | Alceste Scalas | Contract-Oriented Computing in CO2. I will talk about CO2, is a process calculus which models systems of agents that dynamically advertise contracts (i.e., service specifications), reach agreements upon them, and then interact. Unlike other approaches, CO2 does not assume that agents will always behave as promised: it allows to model contract-based interactions that may fail, and in such cases it allows to establish which agent is "culpable" for violating a contract. I will give some hints on a type discipline for "honest" agents — i.e. those that will never violate a contract in any context (even in presence of other agents who actively try to make them fail). |
9:40 - 10:00 | Arthur Azevedo de Amorim | A verified information-flow architecture |
10:10 - 10:20 | Clean up | The lecture hall is used for doctoral defenses and other events during the day, so I've promised to leave it as least as clean and orderly as we find it. |