From: Amin Timany <amintimany@gmail.com>
To: types-announce@lists.seas.upenn.edu, coq-club@inria.fr,
agda@lists.chalmers.se, categories@mta.ca,
logic@math.uni-bonn.de, lean-user@googlegroups.com,
homotopytypetheory@googlegroups.com, eutypes@cs.ru.nl
Subject: [HoTT] Two PhD Positions in Program Verification
Date: Wed, 25 Jul 2018 10:31:34 +0200 [thread overview]
Message-ID: <7D62D57E-4A61-4351-B4D6-33D427828A50@gmail.com> (raw)
[-- 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 --]
reply other threads:[~2018-07-25 8:31 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=7D62D57E-4A61-4351-B4D6-33D427828A50@gmail.com \
--to=amintimany@gmail.com \
--cc=agda@lists.chalmers.se \
--cc=categories@mta.ca \
--cc=coq-club@inria.fr \
--cc=eutypes@cs.ru.nl \
--cc=homotopytypetheory@googlegroups.com \
--cc=lean-user@googlegroups.com \
--cc=logic@math.uni-bonn.de \
--cc=types-announce@lists.seas.upenn.edu \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).