From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.181.75 with SMTP id c11mr500164ywk.57.1489545138994; Tue, 14 Mar 2017 19:32:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.6.207 with SMTP id f76ls414657ioi.6.gmail; Tue, 14 Mar 2017 19:32:18 -0700 (PDT) X-Received: by 10.99.116.18 with SMTP id p18mr520077pgc.119.1489545138200; Tue, 14 Mar 2017 19:32:18 -0700 (PDT) Return-Path: Received: from mail-qt0-x22e.google.com (mail-qt0-x22e.google.com. [2607:f8b0:400d:c0d::22e]) by gmr-mx.google.com with ESMTPS id x124si69137ywb.1.2017.03.14.19.32.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 14 Mar 2017 19:32:18 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) client-ip=2607:f8b0:400d:c0d::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@cmu-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:400d:c0d::22e is neither permitted nor denied by best guess record for domain of awo...@andrew.cmu.edu) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qt0-x22e.google.com with SMTP id n21so3045215qta.1 for ; Tue, 14 Mar 2017 19:32:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cmu-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=qffiI8Ts9Pt/tsEGVc6NKSu1cFnnyJOK8wxr2bq+Qzc=; b=mjKMuI/0cuYBrN3HYPdnKWG1lzPpGYkEZseOjQpL8rHwpG3Xg4gdFBh9lzTTUw5jl6 rU3T7QBPtNpPj9SnviaqYEv94Nb70Rmwa4XG0WLziYlZ9Y14urUfz3yaDuVS21CWCVaw hLd6VmAkABIPotyi1VD2m75p/Qh0cbO8niId0uT4nB2138z5eOGAkNz9+9pzaGl2qKN4 GMTbRZMMnBs8sZOkLpzW7twNc7+EE8XszMzZcCZWUBhmHGfY2duDEmHTUqC60BMEv4Xq 24eahQRGlLoLSvrLxlIkm9mURjyw+Cjlg73pJXFOODqafsjGnDo24AEICDR6w13c54VZ biLQ== X-Gm-Message-State: AFeK/H3bIfh9PPHAkcBT1hscs4z/1p5NXwgQz5sDcnGpzNFvmq7ZWb6+JRJo4l6xbe0zko1s X-Received: by 10.200.57.161 with SMTP id v30mr708193qte.129.1489545137841; Tue, 14 Mar 2017 19:32:17 -0700 (PDT) Return-Path: Received: from steveawodeysair.home (pool-98-111-244-8.pitbpa.ftas.verizon.net. [98.111.244.8]) by smtp.gmail.com with ESMTPSA id o190sm359869qkc.65.2017.03.14.19.32.17 (version=TLS1 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Tue, 14 Mar 2017 19:32:17 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Seeking a lecturer for 8 hrs on proof-assistants in Padua From: Steve Awodey In-Reply-To: <58C80D22.5020708@math.unipd.it> Date: Tue, 14 Mar 2017 22:32:16 -0400 Cc: Maria Emilia Maietti Content-Transfer-Encoding: quoted-printable Message-Id: <5D509F57-2836-465A-A22C-8F5C7287C59D@cmu.edu> References: <58C80D22.5020708@math.unipd.it> To: Homotopy Type Theory X-Mailer: Apple Mail (2.2104) =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=20 Seeking a non-Italian lecturer to give an 8-hour introduction to proof-assi= stants in Padua =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94= =E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2= =80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=E2=80= =94=E2=80=94=E2=80=94=E2=80=94=E2=80=94=20 We are looking for a non-Italian scientist (even a PhD student with high ex= pertise)=20 to give 2 or more seminars, for a total of 8 hours maximum and 4 hours mini= mum=20 (can be split from 2 up to 4 days) as an ***introduction to the use of a proof-assistant based on a constructive de= pendent type theory***=20 like Calculus of Inductive Constructions or Martin-Loef's type theory. =20 Period of seminars: To be chosen in April-May 2018=20 Location: University of Padua=20 Type of students: Master students in Computer Science at the University of = Padua=20 Compensation: 1500 euros=20 DEADLINE for application : 22 March 2017=20 If you are available please write, with a CV included, no later than 22 Mar= ch, to: Maria Emilia Maietti, mai...@math.unipd.it Giovanni Sambin, sam...@math.unipd.it=20 Many thanks for your attention. Best wishes, Maria Emilia Maietti=20 Giovanni Sambin=20