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=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-yb1-xb3c.google.com (mail-yb1-xb3c.google.com [IPv6:2607:f8b0:4864:20::b3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2a850aec for ; Mon, 3 Dec 2018 15:29:59 +0000 (UTC) Received: by mail-yb1-xb3c.google.com with SMTP id s18-v6sf8293678ybm.16 for ; Mon, 03 Dec 2018 07:29:58 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1543850998; cv=pass; d=google.com; s=arc-20160816; b=wZ/XSBd+VIe4ST2wv+N+/2lB2e8b54kXhyTQGL/4pvj70huXuKAUTPnl7ST1Xt0Rro 8lzpgIM6b5iZdfjXshiIrB9VXlWPfEsneE7TgquDMkDZXTE18cxJ5cFum3TDvAfYkRoG UCo0gFSO4U15IuiHrf8BpBLFy+knBevxIRi1RaFnqgoIrzWCHmZniARo9niK1Pfkl17f DkEtHu+YdJfR7Vnm/sZZWWTOFX3qqulrmEwz+mlCKnPLJ8AmGDl9bi/TYTexqHHC/vTy o1CqbANpN82EUzU2jr8TZjmFlflZz+NOgQJZMjKBnqfJZm3aTheYBORL3SkO1iFsvFCr nFCQ== 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:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=c1j58Y5xNYeB8yMMtsQNYEKMkqiLBk4B1DtDInQkGw8=; b=Fv4T1KgOjNjeFUdh8XRXB+wVqCw2vCQjOqXRKkhEJpP5b45BPdCTERoB/007SpLNoS S4TZqspzLSaSlXZueNmrSkbrjywrLnyEZVCPE+PtdjOspS0L39BS6GAKc966D0DjB/9f ts4I8YtXO58lqDcDdTolKtjKXGODX/rfT7DHsMW/yq0UK8CZabRrVIhcn6qdDkjqu4jg M85edswOeGe8kVkpxo7fIAHl3FXlc4aJ/HybQ24JPkLwiYoscGDU7pbKCnf+RciPIozV lj6CXT2rQAGfp/bcc4qcRYwIR6O2Wf0dfTqjfpKeM5h9dytI6uqvNaDHs0waD+CLmCpM 9Ffg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=etZHGiXn; spf=pass (google.com: domain of ana.agvb@gmail.com designates 2607:f8b0:4864:20::62b as permitted sender) smtp.mailfrom=ana.agvb@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:mime-version:references:in-reply-to:from:date:message-id :subject:to:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=c1j58Y5xNYeB8yMMtsQNYEKMkqiLBk4B1DtDInQkGw8=; b=jH3UqXhJClhGa2acTWEF6QNtYEYShtmh8qs92Y14d0bJY02Db14/jdlSjwkm9lomTR AIjQYs8632kFxey1tJhItyJi7H9S2El7ROjjoTBjAHFbhrfMXqjj0RfTG+QJ5cJsQHx3 jwdXahkEdOduPZXl1EtODLQioxRVPg2yvNhX8/P+hIeeAHQJlK6WaFpn6jLcs7f9biYM CesoD8rFETZxSD66ln+/fnDQk3JtRNEeLBarNOgx1UveF+j5pDG28bfGrhEoMjHq1pLn Jnky1OBz1YebHVi1i2v5kjCo2v7XcNuq5/OJ6OOZNYzM5aqSA0wG75Hnj2Pu7Bjyol3F a8Bg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=c1j58Y5xNYeB8yMMtsQNYEKMkqiLBk4B1DtDInQkGw8=; b=TJGOs0JND2jGQoO3HY+VmLDlgfcle/6eZKKdS9qhTtk3FSrpzhJQ9QmPgwMZm+ipc+ I+BxWOlcRMQhagPR1/ss4hgVQVaZGTxy3BfpWzTDm5xtzwvYKsKM1Q+copvVZP/XspE3 7GPv9Km8QFsng8cC5mFvQe3Q5lNf+YMtsVKOM8GSs2zCqbl3niwPLCe9QF2cgo65XtZb YwBckfg2vip5dm8Ry4gqUn2rWAUm0bmj/EQLGihbFJ/pQnA08ibil0PTH74dYmtJD3qa 4LRVgIX/HJLbeB7c7ZBdI67oMmfLCJagQa/I2+k96RNlz6/zPIQguKa9pwc2Y98v44oF feKA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject: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=c1j58Y5xNYeB8yMMtsQNYEKMkqiLBk4B1DtDInQkGw8=; b=aZWYMAWYjh1XLjAylCEGl6c+MMu95HWXD78CWpKuf1pq+6CdTwqV6EX0SYK0U6iz77 6tOYGsF8j6f/rNAJqriXncFlRqlTv2wFCkh7XvnXU+B6dYP68mIaW21XMCx5YVlIXdZN UFfLYDV3At3lgEfiHLIbilBf77rJ8Ke63hEm8kflD5bC8dH+ClysrvwYPlwaK9L33DzB 50/27XCU66e3qXsxg1d8vFylCNBdSZeY6Eqp1QPs27e56rMa66TEx47vg7yCGje/0xIv E+nu/DKwsOtsD5F+xDq6YN8VMfIKWRZq2GGVLWbHcxp7GtWL6drIOlNBu/qz7wKmZ29r TuIQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWYNuCLm5q+r5AukQ2yWHr9OdxNi5IW3pbFZ35Wh4kvaJ1JMWm5y gfFL4KW72gFaDkBYjP1V9xA= X-Google-Smtp-Source: AFSGD/XbGbMdavTcHKL1oaFuhOvWy0zkXm/kX6zd2DlkqnZ+tBtIMmRODn2/r4M424PffehspoPL2g== X-Received: by 2002:a81:115:: with SMTP id 21mr225941ywb.7.1543850997984; Mon, 03 Dec 2018 07:29:57 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0d:d449:: with SMTP id w70ls8426920ywd.6.gmail; Mon, 03 Dec 2018 07:29:57 -0800 (PST) X-Received: by 2002:a81:4901:: with SMTP id w1mr9643428ywa.4.1543850997679; Mon, 03 Dec 2018 07:29:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1543850997; cv=none; d=google.com; s=arc-20160816; b=T71xb/b+rSLhbgoa8FJtQk5S+j3Jl9qWe9eZzZq+2loHHqAtYNArk/Ar43gZ9f8+a/ KSuKHIp3Q0ZSIZjnTe9LpBTlzCwBeWtiWkT1aqh9yATpqpQdpOoaqnH+SBx1P9HHBJ6f SPHAon1ng+nRNH/0YsV/JqKjwfnf7649JKaF6YCLXE9BjhnomAPkkjgNs+jtUjK3RpKC cr05D/WesrzvHWpl8avyQgUnEWyGbhrUsqmBhS/AQpel87tPCtLp6eV18TXTqEajDTG4 /TRbpG5YjbGWBmyh4Rm4BTbAtjLaOd+rykKBvTTnC5PmVWOeoUvFT6hforOTpzOZ8/P8 WI4A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=ozFeh6CVzestRDYzDxYHtZ7T8Xkpm1JePwK32f038nM=; b=JYABmRdlLfMcjXxr4Os7CONxXGut6szVbgWQc7j1DJd0hMZpSUce3+JVvibXq2Z0C0 vnhETke0O0aq/FlXYi80EyJKWTX1icBDAGDsNUK22XH1gsXq0p1zlI757lQ4fUP1nK2I dLiewfy+3SkGJWvsJJ7VStdw2TzrhNzwS4C6kI4Bes27p7PvbiXHcmt7023crP060scu cguOnCdqqDMGz+YVRcTXfaQIzdGNwHQ3msHZ99tFTY4ztXbUI5Rs4H+vDvW81NahMfON lSR+kC1SgF3D4+O5Yk7v9Ptkz5/1/v7Kym175BEM4cLhLm8dp6veWZK/SxeXSpY/7ssH gE7g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=etZHGiXn; spf=pass (google.com: domain of ana.agvb@gmail.com designates 2607:f8b0:4864:20::62b as permitted sender) smtp.mailfrom=ana.agvb@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pl1-x62b.google.com (mail-pl1-x62b.google.com. [2607:f8b0:4864:20::62b]) by gmr-mx.google.com with ESMTPS id z185si230059ywa.3.2018.12.03.07.29.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 03 Dec 2018 07:29:57 -0800 (PST) Received-SPF: pass (google.com: domain of ana.agvb@gmail.com designates 2607:f8b0:4864:20::62b as permitted sender) client-ip=2607:f8b0:4864:20::62b; Received: by mail-pl1-x62b.google.com with SMTP id b5so6648368plr.4 for ; Mon, 03 Dec 2018 07:29:57 -0800 (PST) X-Received: by 2002:a17:902:4827:: with SMTP id s36mr15842409pld.168.1543850996506; Mon, 03 Dec 2018 07:29:56 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Ana Date: Mon, 3 Dec 2018 16:29:44 +0100 Message-ID: Subject: [HoTT] Fwd: Job opening: post-doctoral research and development position at the University of Barcelona To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="0000000000003ba657057c1fd241" X-Original-Sender: ana.agvb@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=etZHGiXn; spf=pass (google.com: domain of ana.agvb@gmail.com designates 2607:f8b0:4864:20::62b as permitted sender) smtp.mailfrom=ana.agvb@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: , --0000000000003ba657057c1fd241 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We are looking for a senior researcher and project manager who has (a significant subset of) the following: - PhD in Mathematics, Computer Science, or a related area - Proficiency in Coq - Knowledge of OCaml - Experience in software design - Experience in formal verification of software with Coq - Experience with SSReflect and the Mathematical Components library Furthermore, the following would be welcome: - Knowledge of Proof Theory and/or Type Theory - Knowledge of other proof checkers besides Coq - Knowledge of other functional languages besides OCaml - Experience with legal texts - A strong track record in research publications The successful applicant will be expected to: - Conduct cutting-edge research, aiming for constructive interactions with other members of the group. Suggested research areas include (but are not restricted to) proof-theory, type theory, modal logic, ordinal analysis, fragments of first and second order arithmetic, proof assistants, automated theorem provers, and related areas. - Supervise a team that develops verified legal software - Supervise PhD students. We are an active and diverse team, lead by Dr. Joost J. Joosten, which comprises several PhD and Master students with a background in Mathematics and Philosophy, among others. Our group's research involves, but is not limited to: proof theory (pure and applied), provability, interpretability and other modal logics, fragments of first and higher-order arithmetic, algebraic logic, formalized meta-mathematics, and ordinal analysis. We are based in the Philosophy Department of the University of Barcelona, located in the city center of Barcelona. Our PhD students are all enrolled in the doctorate program of mathematics and computer science. Most of us are also affiliated to the Institute of Mathematics of the University of Barcelona and to the Barcelona Graduate School of Mathematics. In our applied proof theory group we are developing an industrial product with social impact value for the legal infrastructure of transport of people and goods by road. The project is financed by the European Regional Development Fund and the Ministerio de Ciencia, Innovaci=C3=B3n y Universid= ades. Our software is developed using formal methods, with the goal of high reliability in mind. We are using Coq as our main tool. The working language is English. No knowledge of Spanish or Catalan is necessary. We offer: - A competitive salary - A thriving work environment - Direction over PhD students We encourage international applicants who are enthusiastic about formal verification and supervising a team. Please e-mail your CV to Ana Borges , preferably including an expression of interest and relevant background. We look forward to having you on board! Ana Borges --=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. --0000000000003ba657057c1fd241 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We are looking= for a senior researcher and project manager who has (a significant subset = of) the following:
- PhD in Mathematics, Computer Science, or a related area
- Proficiency in Coq
- Knowledge of OCaml
- Experienc= e in software design
- Experience in formal verification of softw= are with Coq
- Experience with SSReflect and the Mathematical Com= ponents library

Furthermore, the following would b= e welcome:
- Knowledge of Proof Theory and/or Type Theory
- Knowledge of other proof checkers besides Coq
- Knowledge of= other functional languages besides OCaml
- Experience with legal= texts
- A strong track record in research publications

The successful applicant will be expected to:
- C= onduct cutting-edge research, aiming for constructive interactions with oth= er members of the group. Suggested research areas include (but are not rest= ricted to) proof-theory, type theory, modal logic, ordinal analysis, fragme= nts of first and second order arithmetic, proof assistants, automated theor= em provers, and related areas.
- Supervise a team that develops v= erified legal software
- Supervise PhD students.

We are an active and diverse team, lead by Dr. Joost J. Joosten, w= hich comprises several PhD and Master students with a background in Mathema= tics and Philosophy, among others. Our group's research involves, but i= s not limited to: proof theory (pure and applied), provability, interpretab= ility and other modal logics, fragments of first and higher-order arithmeti= c, algebraic logic, formalized meta-mathematics, and ordinal analysis. We a= re based in the Philosophy Department of the University of Barcelona, locat= ed in the city center of Barcelona. Our PhD students are all enrolled in th= e doctorate program of mathematics and computer science. Most of us are als= o affiliated to the Institute of Mathematics of the University of Barcelona= and to the Barcelona Graduate School of Mathematics.

<= div>In our applied proof theory group we are developing an industrial produ= ct with social impact value for the legal infrastructure of transport of pe= ople and goods by road. The project is financed by the European Regional De= velopment Fund and the Ministerio de Ciencia, Innovaci=C3=B3n y Universidad= es.

Our software is developed using formal methods= , with the goal of high reliability in mind. We are using Coq as our main t= ool.

The working language is English. No knowledge= of Spanish or Catalan is necessary.

We offer:
- A competitive salary
- A thriving work environment
=
- Direction over PhD students
We encourage international app= licants who are enthusiastic about formal verification and supervising a te= am.

Please e-mail your CV to Ana Borges <ana.agvb@gmail.com>= ;, preferably including an expression of interest and relevant background.<= /div>

We look forward to having you on board!
= Ana Borges

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