From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,PDS_NO_HELO_DNS,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x33c.google.com (mail-wm1-x33c.google.com [IPv6:2a00:1450:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 11ce2f9d for ; Fri, 12 Jul 2019 10:31:32 +0000 (UTC) Received: by mail-wm1-x33c.google.com with SMTP id 17sf2498859wmj.3 for ; Fri, 12 Jul 2019 03:31:32 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :accept-language:content-language:user-agent:mime-version :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=008VPIVGeIsTo5XXNlMUyMawKJN++mq9MJQmRqaa6wE=; b=snWOXmnxs0Z4O1oEcsWb+U39kPNWhNQ7eFBckspluGRteg22DGHPGaPJzo/nmwt0bp UXhSL11+9VwwZ9I9XGtmfqx+e0kNKqWkQlLrWBx4y7+petzJW9emXp6yzv7oyHuB6Awe tkXshIhdSPC5sJDUvr61mF1JX1wO0npYqH1JDt2sY36A/RXkhFkbS2Wy+aN5Ec1hIHM8 8UCgp9fu9wW318OxdaGZrx1mj9fM0A07TwnEBcrlHKyiWw/8H6zBoUki7O0v+zz/zVsT 1Fpg2f0ZVnOnzODVhpELq9lv+5T5lYENNbvOhoNWtuGrvi8VqNY0ZfY40iDf8ZbA8nIX rYJQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:accept-language:content-language:user-agent :mime-version: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=008VPIVGeIsTo5XXNlMUyMawKJN++mq9MJQmRqaa6wE=; b=j9usN00qjp+vAbohqO4prsHFpVuDGUvT2np9g0++4Bq6E8Z9jl3kmX+0TEoyUs27yR XC4rif6nMNtyiJ1raWHMOd+EwOwlPoJOadTpUBfzCcMO09PeA7dRiHadCPzBkX3jnZh1 QiQjX1TZQCVie86Z+yF6L3crFa5OfzrYvTGvaDxb6OoxPyGG76m/JYi70WIzclgE0edK bSnpcQruyuWxMHq35Sjo5G+6JDqusi+hAxEgMvQmF+ZCKo6gcEK+VoQwjKOTLHZ29+ep GcX+npWs3e91MG5/ysAMnGYnIjNwPflMliy2zeTcJ7DXTRBYVeT28Lf14u35iHnsordp AaBQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU5/BPgB02zOlD3YC73gmFaAN5YflzD8KG706s8z0SZnUXEl4bn QVcRcPv46txoDJTq6afdhcs= X-Google-Smtp-Source: APXvYqwdlFdJnlW6nLwrZOAjvNA3b2px+jtoxkIf1tyfIqfAj5QNHFKGuhWnjV8xdI1lT9Fnp1geKg== X-Received: by 2002:a5d:428b:: with SMTP id k11mr10593341wrq.174.1562927491508; Fri, 12 Jul 2019 03:31:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:adf:db44:: with SMTP id f4ls2974400wrj.15.gmail; Fri, 12 Jul 2019 03:31:30 -0700 (PDT) X-Received: by 2002:adf:eacf:: with SMTP id o15mr11522404wrn.171.1562927490418; Fri, 12 Jul 2019 03:31:30 -0700 (PDT) Received: from uidappmx05.nottingham.ac.uk (uidappmx05.nottingham.ac.uk. [128.243.43.128]) by gmr-mx.google.com with ESMTPS id e12si479102wma.2.2019.07.12.03.31.30 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 12 Jul 2019 03:31:30 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) client-ip=128.243.43.128; Received: from uidappmx05.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 36E706D1009_D286182B for ; Fri, 12 Jul 2019 10:31:30 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx05.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id B5FDC6F69DA_D286181F for ; Fri, 12 Jul 2019 10:31:29 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp4.nottingham.ac.uk with esmtps (TLSv1.2:AES128-SHA256:128) (Exim 4.85) (envelope-from ) id 1hlspt-0005Rw-MD for homotopytypetheory@googlegroups.com; Fri, 12 Jul 2019 11:31:29 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by exchangeSMTP.nottingham.ac.uk (10.159.172.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Fri, 12 Jul 2019 11:31:29 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1531.3; Fri, 12 Jul 2019 11:31:29 +0100 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3 via Frontend Transport; Fri, 12 Jul 2019 11:31:29 +0100 Received: from EUR02-HE1-obe.outbound.protection.outlook.com (128.243.226.54) by exchangeSMTP.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_RSA_WITH_AES_128_CBC_SHA256) id 15.1.1531.3; Fri, 12 Jul 2019 11:31:29 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=RrwSKdYczNMngkSjvzwFQhilHRjLkGGUZY1mzME7PWGw5fh0h+9SYKHLRDLiABoguyuLYIHgJ+xEWpFflk10Tcg+2w+VcX/2jHZjDOaKjEdxa9rG4zXYBg6j6A3uM/9RQ0mkUbHBy6VLz+SuQ1e0uWhF0t+3m4d2KgZXADe8HoVRZU9fmzqNyGoBAoNEoYmwbuq+8t2OJOCFgBYsrYde8yufcgizfQELLm3UnXIsy0gKNXUe7odC/o/qvzvDTZzARWj0T899ffv0MDpMSilJdOIPkYR3J5w6aXpt3yXtcHIa2lx4qMzh3vVke8WI8q2t5eZWPSGTEFFmLWgDvnk2fA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=RYXyM1UQ+iMbbgoVLTjx//iNh0wgEp626VT/yenC44w=; b=f1OPDgcgEDM7YUeQXVIkosPDvv60WidBY7X+CRLumgkG0UqvwyVBH9yvkxAOyl9aFi0sQR/Ki7Sp550O/AeoEwwLlnHr5ny2FMJ1dx8MSziDxpJ4whErT1psvDv5azIGfQtw70Q+f04YPk6JpCai0qbZokMDvSAwJy8ccrbR2e0IjyW+KBORoS9XF7Vc3JR4G5e1f50DUzVs/1DOjl8kCNig8nX1afOMS6rmHhK2P4PssmEKuuhRhtAztyt1dAFDCgGmUA0RKGChBfVe/lEhWvF8C7MIZwV7jdIMvmh6jSSZlcY9spQLpqJDAyXxQBKRauhbJD0KcSFV3qyh/ZvyYg== ARC-Authentication-Results: i=1; mx.microsoft.com 1;spf=pass smtp.mailfrom=exmail.nottingham.ac.uk;dmarc=pass action=none header.from=exmail.nottingham.ac.uk;dkim=pass header.d=exmail.nottingham.ac.uk;arc=none Received: from AM0PR06MB4020.eurprd06.prod.outlook.com (52.133.59.23) by AM0PR06MB6161.eurprd06.prod.outlook.com (20.179.252.158) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2073.10; Fri, 12 Jul 2019 10:31:27 +0000 Received: from AM0PR06MB4020.eurprd06.prod.outlook.com ([fe80::c47e:1c1:29a1:a316]) by AM0PR06MB4020.eurprd06.prod.outlook.com ([fe80::c47e:1c1:29a1:a316%3]) with mapi id 15.20.2052.020; Fri, 12 Jul 2019 10:31:27 +0000 From: Thorsten Altenkirch To: Homotopy Type Theory Subject: [HoTT] Types summer school 2019 at lake Ohrid Thread-Topic: Types summer school 2019 at lake Ohrid Thread-Index: AQHVOJz2+36NCfZ7+katDgomrkQwTA== Date: Fri, 12 Jul 2019 10:31:27 +0000 Message-ID: <31D1008D-B1B3-48C3-B63D-47A4784518C7@nottingham.ac.uk> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Microsoft-MacOutlook/10.1a.0.190609 x-originating-ip: [213.208.157.35] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: caf41209-5fe5-4c64-35ce-08d706b418c8 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600148)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:AM0PR06MB6161; x-ms-traffictypediagnostic: AM0PR06MB6161: x-ms-exchange-purlcount: 1 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:9508; x-forefront-prvs: 00963989E5 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(136003)(366004)(376002)(39860400002)(346002)(396003)(65514003)(189003)(199004)(76116006)(9686003)(66946007)(64756008)(66446008)(2906002)(68736007)(236005)(91956017)(66556008)(6306002)(66476007)(6512007)(53366004)(6116002)(54896002)(99286004)(14444005)(790700001)(7736002)(6486002)(476003)(71200400001)(606006)(71190400001)(478600001)(6436002)(3846002)(53376002)(6916009)(25786009)(486006)(86362001)(66066001)(316002)(33656002)(786003)(966005)(81156014)(26005)(81166006)(8676002)(36756003)(8936002)(14454004)(6506007)(53936002)(58126008)(5660300002)(102836004)(186003)(256004)(17000825003)(42522002)(9984715007);DIR:OUT;SFP:1102;SCL:1;SRVR:AM0PR06MB6161;H:AM0PR06MB4020.eurprd06.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: exmail.nottingham.ac.uk does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: 5Zlg+ehYaY0yPyw/hK+7YMRQy6FvOr0Qe1xQ0Kv0aKGu4d9x6O+RQISTpPYu74hnXfK+Ew5I9v5o4GigihgMeW59ASifs6NuyDZvBZmFGVkA5z/QhEmemcZNS1an1wFkVgjkeAO09rTiQro56RfpDNXtGlFKvZcZVN4pAaMBl9gRAlSnvTbRahiY8M7x6W5Vh0zOYpAK8a20iVPHtJLRJ9nHixcdPFMvJJrbH4Q2FbHtkZ1GSuuXUZ5d1qeW38QYhV8MB9bkGu/6KibJPgDIAHXglYOlVUBpWWKc3CG5L+i1BhbGY04QIvMbzwhAYUcRJbaVXzdjtEmhM0c187taUSpLLxQY1tDMTjqw42So+QcLL2VkrRyaWFC2t4kJ6uPw7f4NpGOp7OVmcfHGRuCQba28pNesji4qinFaiiAhhik= Content-Type: multipart/alternative; boundary="_000_31D1008DB1B348C3B63D47A4784518C7nottinghamacuk_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-Network-Message-Id: caf41209-5fe5-4c64-35ce-08d706b418c8 X-MS-Exchange-CrossTenant-originalarrivaltime: 12 Jul 2019 10:31:27.1661 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: Thorsten.Altenkirch@nottingham.ac.uk X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM0PR06MB6161 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; arc=fail (body hash mismatch); spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.128 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=nottingham.ac.uk 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: , --_000_31D1008DB1B348C3B63D47A4784518C7nottinghamacuk_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable ***REMINDER *** Application deadline is on Monday! COST action CA15123 EUTYPES Summer School on Types for Programming and Verification Ohrid, Macedonia, 30 August =E2=80=93 4 September 2019 https://sites.google.com/view/2019eutypesschool/home CALL FOR APPLICATIONS BACKGROUND Types are pervasive in programming and information technology. A type defines a formal interface between software components, allowing the automatic verification of their connections, and greatly enhancing the robustness and reliability of computations and communications. In rich dependent type theories, the full functional specification of a program can be expressed as a type. Type systems have rapidly evolved over the past years, becoming more sophisticated, capturing new aspects of the behaviour of programs and the dynamics of their execution. The aim of this summer school is to provide advanced training, especially to PhD students and early-career researchers, in all aspects of the theory and practice of type theory and applications. LECTURERS AND COURSES =C2=A7 Course 1: Hugo Herbelin: Introduction to lambda calculus & type the= ory =C2=A7 =C2=A7 Course 2: Jesper Cockx: Correct-by-construction programming in Agda =C2=A7 =C2=A7 Course 3 : Yves Bertot: Introductory course on Coq/Gallina =C2=A7 =C2=A7 Course 4 : Xavier Leroy: Proving the correctness of a compiler =C2=A7 =C2=A7 Course 5: Nicolai Kraus: Introduction to homotopy type theory =C2=A7 APPLICATION The capacity of the summer school is up to 40 students. =C2=A7 Accommodation, full board (i.e., including all meals): 5 nights @ = =E2=82=AC35 =3D =E2=82=AC 175. Extra nights cost also =E2=82=AC35. =C2=A7 A maximum of 30 students (PhD students / early-career researchers) from cou= ntries involved in EUTYPES can receive a grant from the COST action to part= ially cover their costs. To apply for a place in the school and a grant, please fill out (as soon as= possible) the form at http://tiny.cc/olbq8y Application deadline: 15 July 2019. Notification of acceptance and funding: continuously, at the latest by 22 July 2019. VENUE Ohrid is a small town on Lake Ohrid in Macedonia, southwest of Skopje. Ohrid is notable for once having had 365 churches, one for each day of the year, and has been referred to as the Jerusalem of the Balkans. Ohrid and Lake Ohrid are on UNESCO's lists of cultural and natural World Heritage sites. The school will be held in the Congress Centre of Ohrid, which is also the accommodation site. TRAVEL Most participants will have to fly to Skopje and then get to Ohrid by bus. WizzAir operates direct flights to Ohrid from Basel-Mulhouse-Freiburg and London Luton. ORGANIZERS Thorsten Altenkirch Herman Geuvers, Marija Mihova This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/31D1008D-B1B3-48C3-B63D-47A4784518C7%40nottingham.ac.uk. For more options, visit https://groups.google.com/d/optout. --_000_31D1008DB1B348C3B63D47A4784518C7nottinghamacuk_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable

***REMINDER ***

Application deadline is on Monday!

 

      &nb= sp;            COST action CA15123 EUTYPES

      &nb= sp;Summer School on Types for Programming and Verification

 =

      &nb= sp;           Ohrid, Macedonia, 30 August =E2=80=93 4 September 2019

 =

     http= s://sites.google.com/view/2019eutypesschool/home

 =

      &nb= sp;                 CALL FOR APPLIC= ATIONS

 =

BACKGROUND

 =

Types are pervasive in p= rogramming and information technology. A type

defines a formal interfa= ce between software components, allowing the

automatic verification o= f their connections, and greatly enhancing the

robustness and reliabili= ty of computations and communications. In rich

dependent type theories,= the full functional specification of a

program can be expressed= as a type. Type systems have rapidly evolved

over the past years, bec= oming more sophisticated, capturing new

aspects of the behaviour= of programs and the dynamics of their

execution.

 =

The aim of this summer s= chool is to provide advanced training,

especially to PhD studen= ts and early-career researchers, in all

aspects of the theory an= d practice of type theory and applications.

 =

 =

LECTURERS AND COURSES

=C2=A7  Course 1: Hugo Herbelin: Introd= uction to lambda calculus & type theory

=C2=A7   

=C2=A7  Course 2: Jesper Cockx: Correct= -by-construction programming in Agda

=C2=A7   

=C2=A7  Course 3 : Yves Bertot: Introdu= ctory course on Coq/Gallina

=C2=A7   

=C2=A7  Course 4 : Xavier Leroy: Provin= g the correctness of a compiler

=C2=A7   

=C2=A7  Course 5: Nicolai Kraus: Introd= uction to homotopy type theory

=C2=A7   

 =

APPLICATION

 =

The capacity of the summ= er school is up to 40 students. 

 =

=C2=A7  Accommodation, f= ull board (i.e., including all meals): 5 nights @ =E2=82=AC35 =3D =E2=82=AC 175. Extra= nights cost also =E2=82=AC35.

=C2=A7   

A maximum of 30 students= (PhD students / early-career researchers) from countries involved in EUTYP= ES can receive a grant from the COST action to partially cover their costs.=

 =

To apply for a place in = the school and a grant, please fill out (as soon as possible) the form at http://tiny.cc/olbq8y

 =

Application deadline: 15= July 2019.

 =

Notification of acceptan= ce and funding: 

     cont= inuously, at the latest by 22 July 2019.

 =

 =

VENUE<= /p>

 =

Ohrid is a small town on Lake Ohrid&= nbsp;in Macedonia, southwest of

Skopje. Ohrid is notable for once having had 365 churches, one for

each day of the year, an= d has been referred to as the Jerusalem of the

Balkans. Ohrid and Lake = Ohrid are on UNESCO's lists of cultural and

natural World Heritage s= ites.

 =

The school will be held = in the Congress Centre of Ohrid, which is also

the accommodation site.<= o:p>

 =

 =

TRAVEL=

 =

Most participants will h= ave to fly to Skopje and then get to&= nbsp;Ohrid by=

bus.

 =

WizzAir operates direct = flights to Ohrid from Basel-Mulhouse-Freiburg=

and London Luton.

 =

 =

ORGANIZERS

 =

Thorsten Altenkirch Herm= an Geuvers, Marija Mihova

 

 


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/31D1008D-B1B3-48C3-B63D-47A4784518C7%40notting= ham.ac.uk.
For more options, visit http= s://groups.google.com/d/optout.
--_000_31D1008DB1B348C3B63D47A4784518C7nottinghamacuk_--