From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7246 Path: news.gmane.org!not-for-mail From: Adam Chlipala Newsgroups: gmane.science.mathematics.logic.coq.club,gmane.comp.science.types.announce,gmane.science.mathematics.categories Subject: Call for papers (deadline change): LFMTP'12 (colocated with ICFP'12) Date: Mon, 02 Apr 2012 10:34:57 -0400 Message-ID: <4F79B911.7030809@csail.mit.edu> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Trace: dough.gmane.org 1333377325 23454 80.91.229.3 (2 Apr 2012 14:35:25 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Mon, 2 Apr 2012 14:35:25 +0000 (UTC) To: isabelle-users@cl.cam.ac.uk, pvs-announce@csl.sri.com, lics@informatik.hu-berlin.de, types-announce@lists.seas.upenn.edu, agents@cs.umbc.edu, Coq Club , categories@mta.ca, twelf-list@itu.dk Original-X-From: coq-club-owner@inria.fr Mon Apr 02 16:35:22 2012 Return-path: Envelope-to: gsmlcc-coq-club@gmane.org Original-Received: from mail1-relais-roc.national.inria.fr ([192.134.164.82]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1SEiLq-0002C2-6n for gsmlcc-coq-club@gmane.org; Mon, 02 Apr 2012 16:35:22 +0200 X-IronPort-AV: E=Sophos;i="4.75,357,1330902000"; d="scan'208";a="152329541" Original-Received: from walapai.inria.fr ([128.93.30.24]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 02 Apr 2012 16:35:21 +0200 Original-Received: from walapai.inria.fr (localhost [127.0.0.1]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q32EZLwm010296; Mon, 2 Apr 2012 16:35:21 +0200 Original-Received: (from sympa@localhost) by walapai.inria.fr (8.13.6/8.12.10/Submit) id q32EZKrC010291; Mon, 2 Apr 2012 16:35:20 +0200 X-Authentication-Warning: walapai.inria.fr: sympa set sender to coq-club-owner@inria.fr using -f Original-Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q32EZHex010276 for ; Mon, 2 Apr 2012 16:35:17 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AskAADe4eU+AHgKVkWdsb2JhbABFDrkCIgEBAQEJCwsHFAUiggsiFQEFMBA9FhgDAgECAUsBDAgCiAULsRaJCZEcBJVhgRGRTlM X-IronPort-AV: E=Sophos;i="4.75,357,1330902000"; d="scan'208";a="138723848" Original-Received: from outgoing.csail.mit.edu ([128.30.2.149]) by mail4-smtp-sop.national.inria.fr with ESMTP; 02 Apr 2012 16:35:11 +0200 Original-Received: from steppenwolf.csail.mit.edu ([128.30.92.221]) by outgoing.csail.mit.edu with esmtpsa (TLS1.0:RSA_AES_256_CBC_SHA1:32) (Exim 4.72) (envelope-from ) id 1SEiLR-0004jD-SZ; Mon, 02 Apr 2012 10:34:57 -0400 User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.1.16) Gecko/20120317 Icedove/3.0.11 X-Loop: coq-club@inria.fr X-Sequence: 3686 Errors-to: coq-club-owner@inria.fr Precedence: list List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: Xref: news.gmane.org gmane.science.mathematics.logic.coq.club:8046 gmane.comp.science.types.announce:2899 gmane.science.mathematics.categories:7246 Archived-At: Apologies for the re-announcement; we've decided to shift the schedule later a bit, as reflected below. ============================================================= Seventh International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'12) http://people.csail.mit.edu/adamc/lfmtp12/ Copenhagen, Denmark, September 9, 2012 Affiliated with the International Conference on Functional Programming (ICFP'12) CALL FOR PAPERS ------------------------------------------------------------- IMPORTANT DATES Paper submission: May 14, 2012 Author notification: June 18, 2012 Final versions due: July 2, 2012 Workshop day: September 9, 2012 ------------------------------------------------------------- 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 two decades. This workshop will bring together designers, implementors, and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressivity and lucidity of the reasoning process. The broad subject areas of LFMTP'12 are: * 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. * Case studies of meta-programming, and the mechanization of the (meta)theory of descriptions of programming languages and other calculi. Papers focusing on logic translations and on experiences with encoding programming languages theory are particularly welcome. Submission and other details concerning the workshop can be found at its website at http://people.csail.mit.edu/adamc/lfmtp12/. Program Committee: Nick Benton (Microsoft Research) Adam Chlipala (MIT, co-chair) Nils Anders Danielsson (Chalmers University) Elsa Gunter (University of Illinois, Urbana-Champaign) Daniel R. Licata (Carnegie Mellon University) Dale Miller (INRIA) Frank Pfenning (Carnegie Mellon University) Carsten Schürmann (IT University of Copenhagen, co-chair) Matthieu Sozeau (INRIA)