Worthington, Christopher (2022) Investigating Audited Computation within Dependent Session Types. Master's Internship Report, Computing Science.
|
Text
Investigating Audited Computation within Dependent Session Types.pdf Download (413kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (129kB) |
Abstract
In this project two areas of research, both rooted in the Curry-Howard correspondence, are investigated in order to potentially combine their different abilities for computational expression. The first area that is explored is dependent session types for concurrent computation where π-calculus processes are strictly typed along with the functional terms that they communicate. The second area uses Justification Logic to type λ-calculus functions then also record and inspect their computational history. An executive summary of both areas is given and then followed up with a speculative summary on how the two can be combined into a system where typed π-calculus processes can communicate audited functional terms.
| Item Type: | Thesis (Master's Internship Report) |
|---|---|
| Supervisor name: | Perez Parra, J.A. |
| Degree programme: | Computing Science |
| Thesis type: | Master's Internship Report |
| Language: | English |
| Date Deposited: | 02 Sep 2022 14:39 |
| Last Modified: | 02 Sep 2022 14:39 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/28651 |
Actions (login required)
 |
View Item |