From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 98AD77EE63 for ; Wed, 22 May 2013 05:06:40 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of brigitte.pientka@gmail.com) identity=pra; client-ip=74.125.82.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="brigitte.pientka@gmail.com"; x-sender="brigitte.pientka@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of brigitte.pientka@gmail.com designates 74.125.82.47 as permitted sender) identity=mailfrom; client-ip=74.125.82.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="brigitte.pientka@gmail.com"; x-sender="brigitte.pientka@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wg0-f47.google.com) identity=helo; client-ip=74.125.82.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="brigitte.pientka@gmail.com"; x-sender="postmaster@mail-wg0-f47.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhkCAFc1nFFKfVIvk2dsb2JhbABXA4M4sA+JM4g4ewgWDgEBAQEHCwsJFAQkgkcjAScSAw0FEANaEgEFASIcC4dnAw8MmzGCdo88hQInDYhYAQUMjwocg0MDlziBKYp3gzsWKYFdgnQg X-IPAS-Result: AhkCAFc1nFFKfVIvk2dsb2JhbABXA4M4sA+JM4g4ewgWDgEBAQEHCwsJFAQkgkcjAScSAw0FEANaEgEFASIcC4dnAw8MmzGCdo88hQInDYhYAQUMjwocg0MDlziBKYp3gzsWKYFdgnQg X-IronPort-AV: E=Sophos;i="4.87,717,1363129200"; d="scan'208";a="18408159" Received: from mail-wg0-f47.google.com ([74.125.82.47]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 May 2013 05:06:40 +0200 Received: by mail-wg0-f47.google.com with SMTP id e11so725615wgh.2 for ; Tue, 21 May 2013 20:06:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; bh=6xjgTUxzpu4hPJgSEbYLZcjd452SvTqrnBO8l96g8TE=; b=EgZcFwPXKZbikkD+T63hWIIbjQMU3j3mD5sLnQysE1f3dpp058cMC5gsEYRgtPYAWX giwgBYZPJhjGwY56wmYL3y2bjNPNEx+N2DolhuHZ93wYUTF9wCuPimD3ZZMwDbHkii7j pkjVz9zTPTVhYS/tRDce3AVEO8nPwUXu/IBunv2/rxDHRZPEvf5HHtfFZsKDM1BYgGBc nc74+xuQfORyTO7iz+EEip1C1/j0p/oNQT7hpVsaRXiNlBq1urQPct4A8mMKKECoqtVj 1ntnxnL4MMw6NlCx32prkoc0xifqHO7S59XgokvQwqFKJ18Mie1shhuL4s2hE/h52OGu U1ig== MIME-Version: 1.0 X-Received: by 10.181.13.112 with SMTP id ex16mr29184433wid.28.1369191999559; Tue, 21 May 2013 20:06:39 -0700 (PDT) Sender: brigitte.pientka@gmail.com Received: by 10.217.140.8 with HTTP; Tue, 21 May 2013 20:06:39 -0700 (PDT) Date: Tue, 21 May 2013 23:06:39 -0400 X-Google-Sender-Auth: Q6uLkL_7tGL-pgRMlEC2XIoI48k Message-ID: From: Brigitte Pientka To: Brigitte Pientka Content-Type: multipart/alternative; boundary=f46d043c06bec44e6904dd45daca X-Validation-by: bpientka@cs.mcgill.ca Subject: [Caml-list] LFMTP'13: Logical Frameworks and Meta-Languages (CFP) --f46d043c06bec44e6904dd45daca Content-Type: text/plain; charset=ISO-8859-1 ===================================================== ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'13) http://complogic.cs.mcgill.ca/lfmtp13 23 September, 2013 Boston, USA Co-located with with ICFP'13 CALL FOR PAPERS ===================================================== IMPORTANT DATES Paper submission: June 14, 2013 Author notification: July 7, 2013 Final versions due: July 18, 2013 ===================================================== 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 framework. The broad subject areas of LFMTP'13 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. * Logical treatments of inductive and co-inductive definitions and associated reasoning techniques. * New theory contributions: canonical frameworks, contextual frameworks, functional programming over logical frameworks. This year's invited speaker are Dale Miller (Inria) and Robert Harper (CMU) . In addition, this year LFMTP will celebrate the twenty years anniversary of the publication of: Robert Harper, Furio Honsell and Gordon Plotkin. A Framework For Defining Logics. Journal of the Association for Computing Machinery, 40(1):143-184, 1993 Program Committee: ================= * David Baelde, ENS * James Cheney, Edinburgh * Adam Chlipala, MIT * Dan Licata, CMU/IAS * Alberto Momigliano, Milano (organizer) * Brigitte Pientka, McGill (organizer) * Nicolas Pouillard ITU * Randy Pollack, Harvard (organizer) * Andrei Popescu, TUM * Florian Rabe, Bremen * Stephanie Weirich, UPenn Submission Details: ============ In addition to regular papers, we also solicit "work in progress" report, in a broad sense. Those do not need to report original or fully polished research results, but should be interesting for the community at large. Submitted papers should be in PDF, formatted using the ACM SIGPLAN style guidelines (9pt format, more details appear on the symposium web page). The length is restricted to 12 pages, except for "Work in Progress" papers, which are restricted to 6 pages. Submission is via EasyChair: https://www.easychair.org/conferences/?conf=lfmtp2013 Proceedings: ============ Accepted (regular) papers will be included in the ACM Digital Library. Authors are encouraged to publish auxiliary material with their paper (technical appendixes, source code, scripts, test data, etc.). Travel Support: =============== Student attendees with accepted papers can apply for a SIGPLAN PAC grant to help cover travel expenses. PAC also offers other support, such as for child-care expenses during the meeting or for travel costs for companions of SIGPLAN members with physical disabilities, as well as for travel from locations outside of North America and Europe. For details on the PAC program, see its web page (http://www.sigplan.org/PAC.htm). --f46d043c06bec44e6904dd45daca Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D
=A0
=A0=A0 ACM SIGPLAN International Workshop on Logi= cal Frameworks
=A0=A0=A0 and Meta-Languages: Theory and Practice (LFMTP&= #39;13)

=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 http://complogic.cs.mcgill.ca/lfmtp13

=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 23 September, 2013 Boston= , USA

=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0 Co-located with with I= CFP'13

=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0=A0= =A0=A0=A0 CALL FOR PAPERS
=A0=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

IMPORTANT DATES

Paper submission:=A0=A0=A0=A0=A0=A0=A0 June 14, 2013
Author notifica= tion:=A0=A0 =A0 =A0=A0 July 7, 2013
Final versions due:=A0=A0=A0=A0=A0= =A0 July 18, 2013

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

Logical frameworks and meta-lan= guages form a common substrate for
representing, implementing, and reasoning about a wide variety of
deduct= ive 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
co= nsiderable research over the last two decades. This workshop will
bring = together designers, implementors, and practitioners to discuss
various a= spects impinging on the structure and utility of logical
framework. The broad subject areas of LFMTP'13 are:


* Encodi= ng and reasoning about the meta-theory of programming
languages and rela= ted formally specified systems.
* Theoretical and practical issues conce= rning the treatment of variable
binding.
* Logical treatments of inductive and co-inductive definitions = and
associated reasoning techniques.
* New theory contributions: cano= nical frameworks, contextual
frameworks, functional programming over log= ical frameworks.

This year's invited speaker are Dale Miller (Inria) and Robert Harp= er (CMU) .
In addition, this year LFMTP will celebrate the twenty years = anniversary of the
=A0publication of:

Robert Harper, Furio Honse= ll and Gordon Plotkin. A Framework For
Defining Logics. Journal of the Association for Computing Machinery,
40(= 1):143-184, 1993


Program Committee:
=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D

* David Baelde, ENS
* James Cheney, = Edinburgh
* Adam Chlipala, MIT
* Dan Licata, CMU/IAS
* Alberto Momigliano, Milano (organizer)
* Bri= gitte Pientka, McGill (organizer)
* Nicolas Pouillard ITU
* Randy Pol= lack, Harvard (organizer)
* Andrei Popescu, TUM
* Florian Rabe, Breme= n
* Stephanie Weirich, UPenn


Submission Details:
=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D

In addition to regular papers, we also soli= cit "work in progress"
report, in a broad sense. Those do not = need to report original or
fully polished research results, but should be interesting for the
commu= nity at large.

Submitted papers should be in PDF, formatted using th= e ACM SIGPLAN
style guidelines (9pt format, more details appear on the s= ymposium web
page). The length is restricted to 12 pages, except for "Work in
Pr= ogress" papers, which are restricted to 6 pages.

Submission is = via EasyChair:

=A0 https://www.easychair.org/conferences/?conf=3Dlfmtp2013<= /a>

Proceedings:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

Accepted (r= egular) papers will be included in the ACM Digital Library.
Authors are = encouraged to publish auxiliary material with their paper
(technical app= endixes, source code, scripts, test data, etc.).


Travel Support:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
Student attendees with accepted papers can apply for a SIGPLAN PAC gra= nt
to help cover travel expenses. PAC also offers other support, such as=
for child-care expenses during the meeting or for travel costs for
companions of SIGPLAN members with physical disabilities, as well as fortravel from locations outside of North America and Europe. For details
= on the PAC program, see its web page (http://www.sigplan.org/PAC.htm).

--f46d043c06bec44e6904dd45daca--