From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCFJNWFBRAERB2PK4DNAKGQE5DSJSMA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-wr1-x437.google.com (mail-wr1-x437.google.com [IPv6:2a00:1450:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id cb67f154 for ; Wed, 25 Jul 2018 08:31:38 +0000 (UTC) Received: by mail-wr1-x437.google.com with SMTP id w2-v6sf3800086wrt.13 for ; Wed, 25 Jul 2018 01:31:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532507497; cv=pass; d=google.com; s=arc-20160816; b=vZBwNmXO1zbm+dEReGjzEQ0A7ogA501if4gkxNwzwSHQKSofIXbByMqRIMuc2wvfOW Qd6okzoCno3OtYclow/NQKBIFSD5aQQH0rWWN2tw6OvPRXnqcQrBzBYMnizSfAyF3oUc d4XN8RreMfaBH64eD1GMsh2iObrILg32Yg4zLYgciTa1iv4KQNH1GZgD/qska9pIBgZt I7Y7XHDzq3b6dU+pY6owZ1bFDJ/KU72jg8LSmBM2eUVd+Zssw8CpUT3fPE5Z8haDKxib 4mlYaaYjRt94gn6SU9gDuqZS5f4JKXrhFuCRcRVvmg036eh0qB6hCQajDhiNMMa7a81D WmCw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:date:message-id:subject:mime-version :from:arc-authentication-results:arc-message-signature:sender :dkim-signature:dkim-signature:arc-authentication-results; bh=Mp9NGbjdZLnoD64Q49qs5rvtHwc3s/ptVTx/XYUbuf0=; b=FSdMADqih2ck6jYY5bMXxYyT+lOYaOqbnsnkoRpjeUsI0aYEo+EkrvhPr3RxbqVHyf TIrkvfIH7RRU1v/pQ/nZC7Jz0Hlq4eD34CJxfMqR0ttc96f5FprgQl2z3iYpmTnhyWe2 xhKLBKuIQ9mgsjK52QJ41khBtlKCQbdzHU3ekJ0qntXNGTLlgDhj7PKRvcppy2qSYe9l 2mWEnnc3BLMbNFzmokuZJl1JBJZJkdszPTst3SlYh1drJzdQSYMQM4calRSdcLmtUTlV VxqC9Srn3j9QmDh7ZzVposqe84UhTKR8PYCmZuNCfGj0rQv48mGFie4VKJ2M+CMhMLDG PSBQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aR6Rjb7+; spf=pass (google.com: domain of amintimany@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=amintimany@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:mime-version:subject:message-id:date:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Mp9NGbjdZLnoD64Q49qs5rvtHwc3s/ptVTx/XYUbuf0=; b=gbk4UXN2Nu/lljHsaF1rPc1vHX1DyE2iv3MAYj/oQaQ0phHn2zmmhOKVaWxfqdiaAR CbNO8pnnJjq+05JFdJaZ70ejD2jgbam/3lZXjLmWP0INdSsIrj0NzmWkenMWcGXClj0j rhfBDScnjpTZczvv1PNaKU+LQ70A5sQqxRPSQAD6ISkTHYQn260FPjsX1YOvbRSc7llh id5TiyU9iRZS377bQNnv1L12WGO4caLzqxLWSuQd4PQj8AwPel1jAZgzZXJqAa/emHMy LClhhbzLd3ZQeZGlXxuZwxz64i4eKUddd1QaH2jpNcFYSxNscgrqb4cU8TGZWFHAHMJs yBhQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:mime-version:subject:message-id:date:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Mp9NGbjdZLnoD64Q49qs5rvtHwc3s/ptVTx/XYUbuf0=; b=rFY8sAef6fdXC9eTAIQxpOPsnpEEXndhLddx2Njuli4Fl6VqVHm01icdof6cs9Xd8K snq95ug9eZU76Lj19u+lYWD0cxgqz4asXky95RsARw+5e8RnooI9pO9pDnlQ6uWLGrlS R7ZgTVsq2pAZgAEnoMXCniNio2PWpBThdPxvK94fl+JfmZJkZS1L42MKVUTBUHj8jCyQ hplw4o+4QkeMEE7ck/hbK3jLmMsA4Rdzvkls/9BFR9sKG5+Zhmg7NZyYujp+m+NYR085 e2Lfpq/npl4yJR2ZKAQrBJGwm3OVOJ6xc5N+tp7mY7s47mHkb4twk7I+PFUbKdtHomuM Vwag== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:mime-version:subject:message-id:date :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=Mp9NGbjdZLnoD64Q49qs5rvtHwc3s/ptVTx/XYUbuf0=; b=heLbMt4+W2uo+62rfNr4dzBapahiLXlUzNqaXSaPjqAeNU/26oVWBZyzbQ2WzRBW5Q US00BcEHdoS3Nls08sM9Lb79khe8YB+CM8RBFLZsCkFoGGQR13O/JMalMK8Xdhc2hrRA +RQZHWmQkxKtM0OVLX8WnyuqrTOz9yWkw1WNTG6nZi50XTBdXON7KdvivfGXUT/YM3kf eeErKsCzl08we21Ogv1XtOElW9oxsIhRCVhp0LUaxF3BCibCKDZBc/kBbuPdp9K79PVY GrCeFm1TJVbcrtnLXcXW1AE7/vqd7ELhd4GLUuwLLJPFPN7WCj11SOQqr7wDogGicUp5 y+zg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHae6gX8kv8EmCJZvwHVa/owKLJ8RxnariRMmihTmtmp0PPMBv2 qlshv04SxPLav6AOVWgWT28= X-Google-Smtp-Source: AAOMgpeRiPpN7KZC9ePSrRYmoDyT2kINPLfJFMvTuyvCXbrALG1gRggDPvQP51DK84iIG/Oub7Icmw== X-Received: by 2002:adf:fec3:: with SMTP id q3-v6mr209358wrs.2.1532507497513; Wed, 25 Jul 2018 01:31:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:7c12:: with SMTP id x18-v6ls1540374wmc.1.gmail; Wed, 25 Jul 2018 01:31:37 -0700 (PDT) X-Received: by 2002:a1c:7302:: with SMTP id d2-v6mr583436wmb.16.1532507497097; Wed, 25 Jul 2018 01:31:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532507497; cv=none; d=google.com; s=arc-20160816; b=JjRKTdXi4/2u4fBy+uzn+eIyP+B2xu79f/ugaAICtLTSIcdTr+3jR+kVy1rvGGyhXv yAMArhyyv5QoHxUnRaAV1m/U/X4v0ku1fgdK93/OekTDxMw429y+A/R0B11aPWOZQurI 5mIqTitpUrc8KFIlTCf60IiUEfhSvWn7jUT5VIm6BmKok1GvyFrwn/XcZb1k+fn7EQ9m D5PXk/aCDQjwwxCguuDTkIGarmKNyQQfnrix1U4Tgmu4mqNw2pCnL8PMJkXRWPmQTBcB msZzajQdTYT5Tfx/a/ve7VYc370CzpuUP/7oQr3P4TVBYM6nn35vl9h2bCGPhns8AYwU Spag== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:date:message-id:subject:mime-version:from:dkim-signature :arc-authentication-results; bh=Nh0vnW9XH/xmnVuq3obl4YfUS8OhCtQXyZuxDtRYF3U=; b=jK1MxmPDCbJhcjt7w49s3A/gsBvD7n0YQu6U3bq0FZ89hFJfiwW19SqqRCvLQxM+V9 pCMlpm3UO5BQTzQo9oxWAeQi+QMJBCc72/vKcQjjidpeP9zKz4awgIo0/2e+1ho3wPjF TlzA75AaO8jUb2th971R502rDinVNGrEXvYYl8gdsNFyH7TFSRQi2uBvRmA2nQ72SovQ HZwr0bo2HnJ6KdMUV6FEkllkYLn+HhOndIevMx5p+B0qJ3kqw5WbEXeDqxu8DyBcxkO2 w0/6C3oz8jKTMcCWl3xPgqj5/SNU4uM0edCg4Msix9oalbwdS7sBavndN4hmCv5yhYmx Eo/w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aR6Rjb7+; spf=pass (google.com: domain of amintimany@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=amintimany@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ed1-x536.google.com (mail-ed1-x536.google.com. [2a00:1450:4864:20::536]) by gmr-mx.google.com with ESMTPS id d12-v6si409132wrs.0.2018.07.25.01.31.37 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 25 Jul 2018 01:31:37 -0700 (PDT) Received-SPF: pass (google.com: domain of amintimany@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) client-ip=2a00:1450:4864:20::536; Received: by mail-ed1-x536.google.com with SMTP id e6-v6so6496631edr.2; Wed, 25 Jul 2018 01:31:37 -0700 (PDT) X-Received: by 2002:a50:9935:: with SMTP id k50-v6mr21247581edb.45.1532507496857; Wed, 25 Jul 2018 01:31:36 -0700 (PDT) Received: from ptr-81mcicjhyahlwkwq61f.18120a2.ip6.access.telenet.be (ptr-81mcicjhyahlwkwq61f.18120a2.ip6.access.telenet.be. [2a02:1811:c1f:4100:8159:c166:2b91:d113]) by smtp.gmail.com with ESMTPSA id d11-v6sm14897506edo.39.2018.07.25.01.31.35 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 25 Jul 2018 01:31:35 -0700 (PDT) From: Amin Timany Content-Type: multipart/alternative; boundary="Apple-Mail=_53A3C53E-E4E8-4546-B9B1-8465026F9D67" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: [HoTT] Two PhD Positions in Program Verification Message-Id: <7D62D57E-4A61-4351-B4D6-33D427828A50@gmail.com> Date: Wed, 25 Jul 2018 10:31:34 +0200 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 X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: amintimany@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=aR6Rjb7+; spf=pass (google.com: domain of amintimany@gmail.com designates 2a00:1450:4864:20::536 as permitted sender) smtp.mailfrom=amintimany@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --Apple-Mail=_53A3C53E-E4E8-4546-B9B1-8465026F9D67 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="UTF-8" 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= PhD Positions in Program Verification We have two open PhD student positions in the program verification group. T= hese positions involve performing research on program verification under th= e supervision of Prof. dr. Bart Jacobs and postdoctoral researcher Amin Tim= any, with the goal of obtaining a PhD within four to five years. PhD studen= ts are expected to publish and present their results regularly at competiti= ve international conferences and journals, which generally involves interna= tional travel, as well as to contribute to the Department's educational obl= igations. Possible topics include: =E2=80=A2 Logical techniques known as "logical relations" for proving prop= erties of advanced programming languages and programs written in those lang= uages, such as compiler correctness, compiler security, correctness of opti= mizations. =E2=80=A2 Developing advanced program logics for reasoning about correctne= ss of higher-order programs with fine-grained concurrency. =E2=80=A2 Developing supporting theories, such as type theory and category= theory, to serve as logical and semantic foundations for program logics =E2=80=A2 Developing supporting tools, such as proof assistants (e.g. Coq,= Agda) and program verification tools (e.g. Iris, VeriFast), including adva= ncing their usability by developing improved automation technologies. Links: =E2=80=A2 Coq: https://coq.inria.fr =E2=80=A2 Iris: https://iris-project.org =E2=80=A2 VeriFast: https://github.com/verifast/verifast =E2=80=A2 Prof. dr. Jacobs: https://distrinet.cs.kuleuven.be/people/bartj = =E2=80=A2 Dr. Timany: https://distrinet.cs.kuleuven.be/people/amin Profile: =E2=80=A2 Strong background in computer science (Master's degree or equiva= lent) =E2=80=A2 Strong background in mathematical logic and/or theoretical found= ations of computer science Interested? Contact Prof. Bart Jacobs (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 no= t hesitate to contact us if you have any questions regarding these open pos= itions. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --Apple-Mail=_53A3C53E-E4E8-4546-B9B1-8465026F9D67 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset="UTF-8" Please feel free to furthe= r disseminate this announcement and forward it to whomever would be interes= ted.

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

PhD Positi= ons in Program Verification

We have two o= pen PhD student positions in the program verification group. These position= s involve performing research on program verification under the superv= ision 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 competi= tive international conferences and journals, which generally involves inter= national travel, as well as to contribute to the Department's educatio= nal obligations. Possible topics include:

=E2=80=A2 Logical techniques known as "logical relations" for proving p= roperties of advanced programming languages and programs written in th= ose languages, such as compiler correctness, compiler security, correctness= of optimizations.
=E2=80=A2 Developing advance= d program logics for reasoning about correctness of higher-order programs w= ith fine-grained concurrency.
=E2=80=A2 De= veloping supporting theories, such as type theory and category theory, to s= erve as logical and semantic foundations for program logics
=E2=80=A2 Developing supporting tools, such as proof as= sistants (e.g. Coq, Agda) and program verification tools (e.g. Iris, V= eriFast), including advancing their usability by developing improved automa= tion technologies.

Links:
=E2=80=A2 Coq: https://coq.inria.fr
= =E2=80=A2 Iris: https:= //iris-project.org
=E2=80=A2 VeriFast: = ;https://github= .com/verifast/verifast
=E2=80=A2 Prof. dr.= Jacobs: https://distrinet.cs.kuleuven.be/people/bartj
=E2=80=A2 Dr. Timany: https://distrinet.cs.kuleuven.be/people/amin=

Profile:
=E2=80=A2 Strong background in computer science (Master's= degree or equivalent)
=E2=80=A2 Strong backgro= und in mathematical logic and/or theoretical foundations of computer scienc= e

Interested? Cont= act Prof. Bart Jacobs (bart.jacobs@cs.kuleuven.be) & Dr. Amin Timany (= amin.timany@cs.kul= euven.be) no later than September 30, 2018. Do not hesitate to con= tact us if you have any questions regarding these open positions.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--Apple-Mail=_53A3C53E-E4E8-4546-B9B1-8465026F9D67--