Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: [HoTT] Types summer school 2019 at lake Ohrid
Date: Fri, 12 Jul 2019 10:31:27 +0000
Message-ID: <31D1008D-B1B3-48C3-B63D-47A4784518C7@nottingham.ac.uk> (raw)

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

***REMINDER ***
Application deadline is on Monday!

                   COST action CA15123 EUTYPES
       Summer School on Types for Programming and Verification

                  Ohrid, Macedonia, 30 August – 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

§  Course 1: Hugo Herbelin: Introduction to lambda calculus & type theory

§

§  Course 2: Jesper Cockx: Correct-by-construction programming in Agda

§

§  Course 3 : Yves Bertot: Introductory course on Coq/Gallina

§

§  Course 4 : Xavier Leroy: Proving the correctness of a compiler

§

§  Course 5: Nicolai Kraus: Introduction to homotopy type theory

§

APPLICATION

The capacity of the summer school is up to 40 students.


§  Accommodation, full board (i.e., including all meals): 5 nights @ €35 = € 175. Extra nights cost also €35.

§
A maximum of 30 students (PhD students / early-career researchers) from countries involved in EUTYPES 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 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. 

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 
where permitted by law.




-- 
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.
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.

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

             reply index

Thread overview: 2+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-06-25  9:09 Thorsten Altenkirch
2019-07-12 10:31 Thorsten Altenkirch [this message]

Reply instructions:

You may reply publically 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=31D1008D-B1B3-48C3-B63D-47A4784518C7@nottingham.ac.uk \
    --to=thorsten.altenkirch@nottingham.ac.uk \
    --cc=homotopytypetheory@googlegroups.com \
    /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

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox