Commit 3f7d527b authored by Sandra Dylus's avatar Sandra Dylus

Update README.md

parent 0248385f
......@@ -2,15 +2,15 @@
## Bachelor
* implement a DSL for probabilistic programming in Curry (see [official unofficial topics](https://www.informatik.uni-kiel.de/%7Emh/lehre/abschlussarbeiten-vorschlaege/themen.html)
and [Functional Probabilistic Programming](https://web.engr.oregonstate.edu/~erwig/papers/PFP_JFP06.pdf))
* implement a functional data structure with [Coq](http://www.cis.upenn.edu/~bcpierce/sf/current/Basics.html )/[Agda](http://learnyouanagda.liamoc.net/pages/introduction.html)/[Idris](https://www.idris-lang.org)/[F*](https://www.fstar-lang.org)
* implement FlatCurry's operational semantics/type system with [PLTRedex](https://redex.racket-lang.org)
* implement inference system of lecture "Prinzipien von Programmiersprachen" with PLTRedex
* adapt first chapters of [Software Foundations](https://softwarefoundations.cis.upenn.edu/current/toc.html) to Idris
* show that [ListT](http://hackage.haskell.org/package/mtl-2.2.1/docs/Control-Monad-List.html#v:ListT) is indeed a monad
* implement a type system and evaluation relation for a simple functional language
with multiple let-bindings
* implement a functional data structure with [Coq](http://www.cis.upenn.edu/~bcpierce/sf/current/Basics.html )/[Agda](http://learnyouanagda.liamoc.net/pages/introduction.html)/[Idris](https://www.idris-lang.org)/[F*](https://www.fstar-lang.org)
* implement the type system and/or semantics of SaLT (a sub-language of Curry)
* implement the type system and/or semantics of CuMin (a sub-language of Curry)
* implement a secure type system for information flow (rough idea; see [Language-Based Information-Flow Security](https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf))
### Past projects
......@@ -23,5 +23,4 @@
* implement operational semantics of Björn's partial evaluator (see [an old version](http://ceur-ws.org/Vol-1335/wflp2014_paper6.pdf))
* implement an type system (first: simple effect system) for Erlang in an existing, experimental "toy"
programming language (see Lasse's & Mike's theses -- to be released)
and implement the underlying type system in Coq
* implement the type system of TypeScript (rough idea; see [Safe & Efficient Gradual Typing for TypeScript](https://www.microsoft.com/en-us/research/wp-content/uploads/2014/07/safets.pdf))
and implement the underlying type system in Coq
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment