[HoTT] Two PhD Positions in Program Verification

[HoTT] Two PhD Positions in Program Verification

[Amin Timany]

[-- Attachment #1: Type: text/plain, Size: 2825 bytes --]

Please feel free to further disseminate this announcement and forward it to whomever would be interested.

Online version: https://distrinet.cs.kuleuven.be/jobs/#program_verification <https://distrinet.cs.kuleuven.be/jobs/#program_verification>

PhD Positions in Program Verification

We have two open PhD student positions in the program verification group. These positions involve performing research on program verification under the supervision of Prof. dr. Bart Jacobs and postdoctoral researcher Amin Timany, with the goal of obtaining a PhD within four to five years. PhD students are expected to publish and present their results regularly at competitive international conferences and journals, which generally involves international travel, as well as to contribute to the Department's educational obligations. Possible topics include:

	• Logical techniques known as "logical relations" for proving properties of advanced programming languages and programs written in those languages, such as compiler correctness, compiler security, correctness of optimizations.
	• Developing advanced program logics for reasoning about correctness of higher-order programs with fine-grained concurrency.
	• Developing supporting theories, such as type theory and category theory, to serve as logical and semantic foundations for program logics
	• Developing supporting tools, such as proof assistants (e.g. Coq, Agda) and program verification tools (e.g. Iris, VeriFast), including advancing their usability by developing improved automation technologies.

Links:
	• Coq: https://coq.inria.fr <https://coq.inria.fr/>
	• Iris: https://iris-project.org <https://iris-project.org/>
	• VeriFast: https://github.com/verifast/verifast <https://github.com/verifast/verifast>
	• Prof. dr. Jacobs: https://distrinet.cs.kuleuven.be/people/bartj <https://distrinet.cs.kuleuven.be/people/bartj>
	• Dr. Timany: https://distrinet.cs.kuleuven.be/people/amin <https://distrinet.cs.kuleuven.be/people/amin>

Profile:
	• Strong background in computer science (Master's degree or equivalent)
	• Strong background in mathematical logic and/or theoretical foundations of computer science

Interested? Contact Prof. Bart Jacobs (bart.jacobs@cs.kuleuven.be <mailto:bart.jacobs@cs.kuleuven.be>) & Dr. Amin Timany (amin.timany@cs.kuleuven.be <mailto:amin.timany@cs.kuleuven.be>) no later than September 30, 2018. Do not hesitate to contact us if you have any questions regarding these open positions.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 4750 bytes --]