From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.178.80 with SMTP id t16mr3775354pgo.45.1492703885752; Thu, 20 Apr 2017 08:58:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.0.7 with SMTP id 7ls1776693ioa.12.gmail; Thu, 20 Apr 2017 08:58:04 -0700 (PDT) X-Received: by 10.36.9.206 with SMTP id 197mr1365258itm.9.1492703884594; Thu, 20 Apr 2017 08:58:04 -0700 (PDT) Return-Path: Received: from mail-yb0-x234.google.com (mail-yb0-x234.google.com. [2607:f8b0:4002:c09::234]) by gmr-mx.google.com with ESMTPS id u66si792509ywg.0.2017.04.20.08.58.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Apr 2017 08:58:04 -0700 (PDT) Received-SPF: pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::234 as permitted sender) client-ip=2607:f8b0:4002:c09::234; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of sojakova...@gmail.com designates 2607:f8b0:4002:c09::234 as permitted sender) smtp.mailfrom=sojakova...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-yb0-x234.google.com with SMTP id 81so31059854ybp.0 for ; Thu, 20 Apr 2017 08:58:04 -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; bh=icrvINDq5J+CjY3MPymuI9jYhY7AIRH0cC7+w//Aq5E=; b=FaI1DogO87PSU2qhZUq+uUvjUGJo9htgjuw1tmXJlbOLFXktl4N+0vKVrctFkoayUJ dNJmqC5MJZHEdI7Wm4fsxfYC1wvCm+D9nN1Oh7DtFEJo4TiGDb4UMg2dilRiXqfCxznX PSKv7PejGg/QEKzLW8Mj3tOEAt33RM6lkU8Vrw7tkFn5vONbzlyDxH1BeZey0MRAVmlf 8TM1GWZkPBVxgGygmNKxd+kyBuqhbmllHoTb+r/KLuzAYcnn+RFx92RU/JGOT99PztUi Hv305SaI+pmRe7LHMPGd/ywhaDGm8mrphDXFDGUuIDtYOq1fhDWNBlIzoPsMuDZ4BEeB jZNQ== X-Gm-Message-State: AN3rC/6jGsabdZMvkBCx++WzXWn5dUR4XyVQcAXPGyTBibScQxU2I6gw 5qQ4mXS5TFVxvlI+NRk= X-Received: by 10.37.173.131 with SMTP id z3mr7696793ybi.64.1492703883970; Thu, 20 Apr 2017 08:58:03 -0700 (PDT) Return-Path: Received: from [192.168.19.1] (host-37-191.ncbocob.boone.nc.us.clients.pavlovmedia.net. [68.180.37.191]) by smtp.gmail.com with ESMTPSA id z188sm2729038ywf.56.2017.04.20.08.58.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Apr 2017 08:58:03 -0700 (PDT) From: Kristina Sojakova Subject: LFMTP '17 (Oxford, UK) Call for papers To: homotopy Type Theory Message-ID: <32931fb5-e3cc-9584-28b0-2046a938be14@gmail.com> Date: Thu, 20 Apr 2017 11:58:47 -0400 User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="------------7244BFDCE9E3E8A942A30643" --------------7244BFDCE9E3E8A942A30643 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Dear all, The workshop on Logical Frameworks and Meta-Languages: Theory and Practice (http://lfmtp.org/workshops/2017/home.shtml) will take place in Oxford on September 8. Please consider submitting! The call for papers is below. Best, Kristina **** LFMTP 2017: Logical Frameworks and Meta-Languages: Theory and Practice **** Affiliated with FSCD 2017 Oxford, United Kingdom, September 8, 2017 Conference website http://lfmtp.org/workshops/2017/home.shtml Submission link https://easychair.org/conferences/?conf=lfmtp2017 ** Important dates: Abstract registration deadline: June 18, 2017 Submission deadline: June 25, 2017 Notification to authors: July 30, 2017 Final version deadline: August 13, 2017 ** Description Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand have been the focus of considerable research over the last three decades. This workshop brings together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable bindings, inductive and co-inductive reasoning techniques, and the expressivity and lucidity of the reasoning process. LFMTP 2017 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: - Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. - Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. - Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. - New theory contributions such as canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, or homotopy type theory. - Systematic translation, combination, and integration of logics or theorem prover libraries. - Applications of logical frameworks, e.g. in certification and guarantee of security properties. - Techniques for programming with binders in functional programming languages such as Haskell, OCaml, or Agda and logic programming languages such as lambda Prolog or Alpha-Prolog. LFMTP 2017 will be also the occasion to celebrate the 70th birthday of Randy Pollack, author of the LEGO proof assistant and many other contributions to this field. ** Submission Guidelines The following paper categories are welcome: - Full papers describing original research and not simultaneously submitted to another journal or conference. - Work-in-progress reports, in a broad sense. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGCONF format. The page limit is 8 pages for full papers, and 4 pages for work-in-progress reports. Submission link is at https://easychair.org/conferences/?conf=lfmtp2017 ** Program Committee Thorsten Altenkirch (University of Nottingham, UK) Kaustuv Chaudhuri (INRIA, France) Gilles Dowek (ENS Cachan, France) Amy Felty (University of Ottawa, Canada) Andrzej Filinski (University of Copenhagen, Denmark) Marino Miculan (DMIF, University of Udine, Italy), co-chair Florian Rabe (Jacobs University Bremen, Germany), co-chair Wilmer Ricciotti (LFCS, University of Edinburgh, UK) Claudio Sacerdoti Coen (University of Bologna, Italy) Kristina Sojakova (Appalachian State University, USA) ** Organizing committee Florian Rabe (Jacobs University Bremen, Germany) Marino Miculan (DMIF, University of Udine, Italy) ** Contact All questions about submissions should be emailed to f.r...@jacobs-university.de --------------7244BFDCE9E3E8A942A30643 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 7bit

Dear all,

The workshop on Logical Frameworks and Meta-Languages: Theory and Practice (http://lfmtp.org/workshops/2017/home.shtml) will take place in Oxford on September 8. Please consider submitting!

The call for papers is below.

Best,

Kristina


**** LFMTP 2017: Logical Frameworks and Meta-Languages: Theory and Practice ****

Affiliated with FSCD 2017 Oxford, United Kingdom, September 8, 2017 Conference website http://lfmtp.org/workshops/2017/home.shtml Submission link https://easychair.org/conferences/?conf=lfmtp2017 ** Important dates: Abstract registration deadline: June 18, 2017 Submission deadline: June 25, 2017 Notification to authors: July 30, 2017 Final version deadline: August 13, 2017 ** Description Logical frameworks and meta-languages form a common substrate for representing, implementing, and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design and implementation on the one hand and their use in reasoning tasks ranging from the correctness of software to the properties of formal computational systems on the other hand have been the focus of considerable research over the last three decades. This workshop brings together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable bindings, inductive and co-inductive reasoning techniques, and the expressivity and lucidity of the reasoning process. LFMTP 2017 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: - Encoding and reasoning about the meta-theory of programming languages and related formally specified systems. - Theoretical and practical issues concerning the treatment of variable binding, especially the representation of, and reasoning about, datatypes defined from binding signatures. - Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. - New theory contributions such as canonical and substructural frameworks, contextual frameworks, proof-theoretic foundations supporting binders, functional programming over logical frameworks, or homotopy type theory. - Systematic translation, combination, and integration of logics or theorem prover libraries. - Applications of logical frameworks, e.g. in certification and guarantee of security properties. - Techniques for programming with binders in functional programming languages such as Haskell, OCaml, or Agda and logic programming languages such as lambda Prolog or Alpha-Prolog. LFMTP 2017 will be also the occasion to celebrate the 70th birthday of Randy Pollack, author of the LEGO proof assistant and many other contributions to this field. ** Submission Guidelines The following paper categories are welcome: - Full papers describing original research and not simultaneously submitted to another journal or conference. - Work-in-progress reports, in a broad sense. Those do not need to report fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGCONF format. The page limit is 8 pages for full papers, and 4 pages for work-in-progress reports. Submission link is at https://easychair.org/conferences/?conf=lfmtp2017 ** Program Committee Thorsten Altenkirch (University of Nottingham, UK) Kaustuv Chaudhuri (INRIA, France) Gilles Dowek (ENS Cachan, France) Amy Felty (University of Ottawa, Canada) Andrzej Filinski (University of Copenhagen, Denmark) Marino Miculan (DMIF, University of Udine, Italy), co-chair Florian Rabe (Jacobs University Bremen, Germany), co-chair Wilmer Ricciotti (LFCS, University of Edinburgh, UK) Claudio Sacerdoti Coen (University of Bologna, Italy) Kristina Sojakova (Appalachian State University, USA) ** Organizing committee Florian Rabe (Jacobs University Bremen, Germany) Marino Miculan (DMIF, University of Udine, Italy) ** Contact All questions about submissions should be emailed to f.r...@jacobs-university.de

--------------7244BFDCE9E3E8A942A30643--