From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.190.65 with SMTP id o62mr353122lff.16.1490819626326; Wed, 29 Mar 2017 13:33:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.213.70 with SMTP id m67ls822074lfg.1.gmail; Wed, 29 Mar 2017 13:33:45 -0700 (PDT) X-Received: by 10.25.213.77 with SMTP id m74mr352877lfg.14.1490819625268; Wed, 29 Mar 2017 13:33:45 -0700 (PDT) Return-Path: Received: from mail-wr0-x244.google.com (mail-wr0-x244.google.com. [2a00:1450:400c:c0c::244]) by gmr-mx.google.com with ESMTPS id x188si737867wmx.0.2017.03.29.13.33.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Mar 2017 13:33:45 -0700 (PDT) Received-SPF: pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::244 as permitted sender) client-ip=2a00:1450:400c:c0c::244; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of benedik...@gmail.com designates 2a00:1450:400c:c0c::244 as permitted sender) smtp.mailfrom=benedik...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-wr0-x244.google.com with SMTP id w43so6324437wrb.1 for ; Wed, 29 Mar 2017 13:33:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:message-id:date:user-agent:mime-version :content-transfer-encoding; bh=piWUInAMV9+8gGTRkHoEA2vsdRUiAUDL27G02qNsvic=; b=sBX/TapqRSYkvxHkCittQ09Cs6oI8Y7B6UJpqU8QzlIQKv2jEU1F0ZrV4tnT9Mlpwm l56B+JBJfwsq43b1olkLCDt4lbVR3u00uXPRhr2/Ew474QRBU3/2XmjRxDVRPjBRGn3r Zhc8ldBe/ExHj0LlWw+zsjCNdCufh1wmQWxXOysAQDSeKzvUwbC86o0CWnuUy9wfWEiP /fX0qTRRF5eFA9ZXv+ETtxRHXgPuy5I/MW53wjj/EhYs5KGoFjZ/o4HHHs1C9w0JO6AH 3QViYjOB+MJvBlAQb9Henky32IcoMrwNlfmiTUiHKlSBcSsAw3kdIgSPZTpdLnWDkEAt vozA== X-Gm-Message-State: AFeK/H1yX2vp/vPzZ7gOLqR3nq7k+21ioFRckCAq8SSByfno2KyjPzXf4b6MSdk0QqxrrA== X-Received: by 10.28.222.4 with SMTP id v4mr229166wmg.75.1490819625031; Wed, 29 Mar 2017 13:33:45 -0700 (PDT) Return-Path: Received: from ?IPv6:2a01:cb05:891c:2d00:6680:99ff:feed:97f7? (2a01cb05891c2d00668099fffeed97f7.ipv6.abo.wanadoo.fr. [2a01:cb05:891c:2d00:6680:99ff:feed:97f7]) by smtp.gmail.com with ESMTPSA id p185sm9542842wme.20.2017.03.29.13.33.43 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 29 Mar 2017 13:33:44 -0700 (PDT) From: Benedikt Ahrens Subject: Call for Contributions: Foundations for Practical Formalization of Mathematics To: homotopytypetheory , eut...@cs.ru.nl, coq-...@inria.fr, ag...@lists.chalmers.se X-Enigmail-Draft-Status: N1110 Message-ID: <8714070d-d59b-9e1d-b1ff-328f1d7ab755@gmail.com> Date: Wed, 29 Mar 2017 22:33:42 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Icedove/45.6.0 MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 7bit Workshop on Foundations for Practical Formalization of Mathematics 26 - 27 April 2017 Nantes, France Meeting in the framework of the COST EUTypes Action (https://eutypes.cs.ru.nl/) # Goals of the workshop Proof assistants are now state of the art tools for formalizing mathematical reasoning, both for the verification of proofs in mathematics itself and for the verification of software and hardware in computer science. The workshop aims to bring together researchers interested in formalizing mathematics and in proof assistants based on dependent type theory, homotopy type theory, higher inductive types and cubical type theory, to discuss how type-based proof assistant can be used for the practical formalization and verification of mathematical proofs. # Call for contributions We encourage talk proposals on the aforementioned topics. To propose a talk, please send an email with title and abstract to Benedikt Ahrens (benedikt DOT ahrens AT inria DOT fr). # Funding Funding for travel and accommodation is available. If you would like to be considered for funding, please mention this in your talk proposal. # Further information Further information is available on https://fpfm.github.io/ .