From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE,URIBL_SBL_A autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-pg1-x539.google.com (mail-pg1-x539.google.com [IPv6:2607:f8b0:4864:20::539]) by inbox.vuxu.org (Postfix) with ESMTP id 2E40823066 for ; Thu, 8 Feb 2024 23:31:45 +0100 (CET) Received: by mail-pg1-x539.google.com with SMTP id 41be03b00d2f7-5cfd94f9433sf262382a12.2 for ; Thu, 08 Feb 2024 14:31:45 -0800 (PST) ARC-Seal: i=3; a=rsa-sha256; t=1707431503; cv=pass; d=google.com; s=arc-20160816; b=UeeWEVPtNvCZ5F/CCd9aJjl/FwU/UhEh/PplWG7uMktzWJeSfZhs6DYG1u7Cs8Pb/O Z/vz6vmhaVrSjGNPmMsp6pnsR8xrOS7EKHiNBVZWXYiY3ZZ73D/J0Kgx87Yu2oEtJ7zp GQ09MYVhdL9YDPFKq5RqcFMANYY+MgH46mIXQVNJzy7kJhpDw49zc2jvtUwPkx4EgAIt ybHUtXmq1Ocdq33f8vgH84ou2xLmKJH99tmQUZUXI4OI7pxLYRp/UzVz/eEldAmqGCNr /VO9TbSm1OGc/Gx8j4+a2GJSq5SziuFS5aRtLAyio2J89h/27OJVrp3V0lY95viRfQc5 ubDw== ARC-Message-Signature: i=3; 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:mime-version:content-transfer-encoding :content-id:user-agent:resent-from:content-language:accept-language :message-id:date:thread-index:thread-topic:subject:to:from:sender :dkim-signature; bh=ii2pUfh891L7B8sx7qzR5Qd7x//ZEmK1Aq2RqWFTjIo=; fh=UHC338aMVYMiPYJEZmyZbNIBpV0+myy76hazOm8qvfA=; b=nI34iA0a0rUDb7ELtwU8bHcTkYRGCQsRcHEsHPlZD8vM6SGWQ53ibVoFwylSC0vAst LMgr0/THIZUeWnBLLBrovSUr/NZ+fEOtSVwOOUaAqk8OTYTjUd/kJK6L8AR14tkwui/b C37U5c6AR3hIgUmEd/MYV8QkhLeANkOVaMdkL0HqlF+lBEBXKZpeAY5oA+R+LALgg7wm O1J/6BMhdO62q8XeKev8Fv26eeSnDHintSQ3G9Wkop20V/gIHqkhUP3rjDJsT5zyEbB1 KXk5X9oKlDQ0ZGE0pflehOy4k05YJ5/qgHHlIYCvN4DLFRwn9VQAOnYAxp5IvKRzTGvH gWNg== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@unibo.it header.s=selector1 header.b=B+2jz9+c; arc=pass (i=1 spf=pass spfdomain=unibo.it dkim=pass dkdomain=unibo.it dmarc=pass fromdomain=unibo.it); spf=pass (google.com: domain of claudio.sacerdoticoen@unibo.it designates 2a01:111:f403:2611::700 as permitted sender) smtp.mailfrom=claudio.sacerdoticoen@unibo.it; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=unibo.it DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1707431503; x=1708036303; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:mime-version:content-transfer-encoding:content-id :user-agent:resent-from:content-language:accept-language:message-id :date:thread-index:thread-topic:subject:to:from:sender:from:to:cc :subject:date:message-id:reply-to; bh=ii2pUfh891L7B8sx7qzR5Qd7x//ZEmK1Aq2RqWFTjIo=; b=xQESp0xkkXyIHdA4EMQPww8bGJg3k5TF4nGOuariTdV7IGj47a0BpzUzE9Dm5cNUEy hCqkzhdRlbFqXHndm9rfLwACXVXMJY/O6+Q7VrRScv577aGvjxdkS7FeNb+LZlApTdXu HM5SSpRjz0p0L6IEUpvxv/U2KWjvII9yW2WFn6yuOdYTYKI4emCIMljNw/agmbQazP5T tVQLQ/5zoC4/gnZxZvVIRjh+z4UhYnGZgT7m/eJppF6PMewnpOPV1Tjq0yH++LT4fmJS EeJC5/vQfT6Ei6FUXvG/68OW+Ov7zdl08dNJPNg3x680tvC9XyYjw2syXs9k9cibPvD6 gTaA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1707431503; x=1708036303; h=list-unsubscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:mime-version :content-transfer-encoding:content-id:user-agent:resent-from :content-language:accept-language:message-id:date:thread-index :thread-topic:subject:to:from:x-beenthere:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=ii2pUfh891L7B8sx7qzR5Qd7x//ZEmK1Aq2RqWFTjIo=; b=EwFD1L4sza545zZL8mY9aRxh99meuuoepyCsvAKxWivwofmL4w9D1PB8E5JleaqGhz wKsf+I+0yCg3qfQx7ZQw4P8mbPCx0lvq1OAqMa1mt+1X1v6zbSCPoHnBbt1Okd0rZi0x EamUjxWQjGqVOuhiCbKNPwAHPzRje4XTHT+JxFUTlewhVCdNV0/pQhZZ65j8QVzIWcO9 z9x+s6yEQXw4/BX3BuW4Ob1BOoKB6r8ReBCv82uaXHSZpzs22DSHX6igxfDITgkVG2Qx uP5BduhS1XfctOn82WCAU7/artag9TVxM6QAeDA0Hkh7RECxaMI85ATaan1k8n4XPpY9 UaIw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOJu0YxsEJe+OwM97GlosSjTuC39d/MfDGm+Vbhy9zL7bxoI+1R0moSn VMrFOuFOEzr5jtbagZnZ/xpkLhJgnrLoXsN4tVGNDM8/HkD9qGao X-Google-Smtp-Source: AGHT+IH4wg7vRWqZS617sNinRG76fgj2qnU6WhO9w8yzjHJDt33GYTn14q9ZTC6rUF6AmSB4ppRC+A== X-Received: by 2002:a05:6a20:b797:b0:19b:81be:34e4 with SMTP id fh23-20020a056a20b79700b0019b81be34e4mr726085pzb.50.1707431502795; Thu, 08 Feb 2024 14:31:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6a00:1d82:b0:6dd:e100:6969 with SMTP id z2-20020a056a001d8200b006dde1006969ls274665pfw.0.-pod-prod-02-us; Thu, 08 Feb 2024 14:31:40 -0800 (PST) X-Received: by 2002:a05:6a00:4e5b:b0:6e0:50c0:11e3 with SMTP id gu27-20020a056a004e5b00b006e050c011e3mr625680pfb.31.1707431500265; Thu, 08 Feb 2024 14:31:40 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1707431500; cv=pass; d=google.com; s=arc-20160816; b=WKhJuP9DwK7N/UgEPaXrKP5BXz1iky7WxmOcRmoPX6WzHFTwVLzjehdFbdLqY2mT3D ylMNwAV2yUR/uqiZsA0nwrBhp6VoFdbpM8Mw+M8BINrWXoYS4vxuQBJfTeMWm/+G5JMI ntZDeBcVUC6rUAV1kRu8HHEAMWstFda9ALJOgy+nt2MUcwRVJiu/0UkACcTdNsdpJgcU 3jmLPpuPdtfKmiZwpr3WF0fBnewDvlHvGDvY+dQGFIBJZ++CGQvtU7lGXG66V7YRVOk6 O3IdvF7qGobIJvOagnsY44WvrY3S6wLGk2yeZr1uh80NVmUn2mrSL5tg2UV4EV8HMmQ6 z6sA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :resent-from:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from:dkim-signature; bh=J0clRYMHwXyKY6fyabXQ7I3+wQ4KAuIgROdfwY8nzwE=; fh=UHC338aMVYMiPYJEZmyZbNIBpV0+myy76hazOm8qvfA=; b=QEh4JNkXUDxdxuTFVdXmgNptivSQPksg6h/pXXgekpYkUAxW+A/iWZTRR7TRGDzcgY zcCb6BWmksH/9S9EwTxrxqWFKkNCAf07jy4tibM8PZjtgBv2T+XcRDsZowNpzqLvUhHo ZPcrxrcSXo5NZXXOSKdauN1OEPO0mKOaGqhhB+yelQOxyFx/RkrKjbFbrZaRxxkVHRbW 0lTdtjI1ZrUaVorts8xjrispkk8p9lH/kqidM3ALVsQl4DmFCG6p6NBdBVQ8lpWYnjLk zH5/9XcuIYGKOeSp+pQBjTPrhodoao+XgFS5gMUJd+I9eR0LZFZSrH65WhMxJyuO7Voy CgkA==; dara=google.com ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@unibo.it header.s=selector1 header.b=B+2jz9+c; arc=pass (i=1 spf=pass spfdomain=unibo.it dkim=pass dkdomain=unibo.it dmarc=pass fromdomain=unibo.it); spf=pass (google.com: domain of claudio.sacerdoticoen@unibo.it designates 2a01:111:f403:2611::700 as permitted sender) smtp.mailfrom=claudio.sacerdoticoen@unibo.it; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=unibo.it X-Forwarded-Encrypted: i=2; AJvYcCVEEuaHwWdeiV90VbxgOK/i4EV2UjKoFgQYISp+Zp1IZsluixak3VracoGuEeecW61UBBEpx2VX3V4c6nGSzRLKupFQTMgOLWXY33IUlLWRH+uatJLTrYMg5YM8RTM1OHW9sMxW8wmfVG8OxOM0sE7q1jD9i8J/ZSBrbqw= Received: from EUR04-VI1-obe.outbound.protection.outlook.com (mail-vi1eur04on20700.outbound.protection.outlook.com. [2a01:111:f403:2611::700]) by gmr-mx.google.com with ESMTPS id k125-20020a632483000000b005dc1683daa5si50282pgk.4.2024.02.08.14.31.39 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Feb 2024 14:31:40 -0800 (PST) Received-SPF: pass (google.com: domain of claudio.sacerdoticoen@unibo.it designates 2a01:111:f403:2611::700 as permitted sender) client-ip=2a01:111:f403:2611::700; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=RyVNGEVrFdBW1E4vWgjcYkfBJyB1HlaP31v1HE6NeeEd3R4zvQw5LZG4WWak4RwFGlKpK5IH/0dtKzmANOAMkEFCUfJCK9rV6YKtTUGGjvl403sm3FEaxy6hjC4eGnj6sWxPcRuFXeGxkj+/r/3OierEgMuCTkRZgnGnJuV9fimH/quk+YoYPl/KT+FHPCKsV/AhFMGF2+8aN9LGTfSk3aXd//m9vjZR7DTnG+7L8Nkf99PiuO5gBI+qdAw2Xce935ygWhURtg95lKXVd7Avfh0JKzNyKrpHHeBSyOTN0w6Z958XLoBCQG2NLKqdclGEhgCDio2X8nFt9fPH+cZHhA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=J0clRYMHwXyKY6fyabXQ7I3+wQ4KAuIgROdfwY8nzwE=; b=gJ1jkEpDAV5uz3OMq/hw/nLXXwJsNQ6XDTY4BdrPmP4ZYFZnZ0/EmedqaG0cHAn7MGIzBtGeKPUUEIDZ9ECBEuvYPxWyrPIUjFD2g8gTmU41sbxBic2foqdwBD/QhWsLBMAy8onEq5ObhbplCVDtVAgWUZ++wAsNiJqQmiggddFiLZgKIxBsGrFbk4Y9Tp5xxosz4xcbxG/veui8ze7glawK6PpRCfZI2N2skMtWRjBcV9Du7ZLn5SbNM1XxbcHxvwErAUjhAacQp0xYjuSaDHe1vU3qnPd6CVRQ0X5c0IzyiVRriyVYjC4paKt9KE/NJSGuDvp8QZxrl+KZl+4ahw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=unibo.it; dmarc=pass action=none header.from=unibo.it; dkim=pass header.d=unibo.it; arc=none Received: from AS8PR01MB7333.eurprd01.prod.exchangelabs.com (2603:10a6:20b:257::6) by AS8PR01MB8859.eurprd01.prod.exchangelabs.com (2603:10a6:20b:40f::9) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7270.27; Thu, 8 Feb 2024 22:31:37 +0000 Received: from AS8PR01MB7333.eurprd01.prod.exchangelabs.com ([fe80::f6ae:118b:685b:cce8]) by AS8PR01MB7333.eurprd01.prod.exchangelabs.com ([fe80::f6ae:118b:685b:cce8%6]) with mapi id 15.20.7249.039; Thu, 8 Feb 2024 22:31:36 +0000 From: Claudio Sacerdoti Coen To: "cl-isabelle-users@lists.cam.ac.uk" , "maude-users@lists.cs.illinois.edu" , "fom@cs.nyu.edu" , "abella-theorem-prover@googlegroups.com" , "homotopytypetheory@googlegroups.com" , "logica-l@dimap.ufrn.br" , Claudio Sacerdoti Coen , "ssreflect@msr-inria.inria.fr" , "why3-club@lists.gforge.inria.fr" , "lfmtp@inria.fr" , "gdr.gpl@imag.fr" , "folli@folli.info" , "prooftheory@lists.bath.ac.uk" , "eutypes@cs.ru.nl" , "alp-diffusion@univ-lille1.fr" , "acl2@utlists.utexas.edu" , "newsletter@aarinc.org" Subject: [HoTT] CfP: Logica Frameworks and Meta Languages: Theory and Practice (LFMTP24) Thread-Topic: CfP: Logica Frameworks and Meta Languages: Theory and Practice (LFMTP24) Thread-Index: AQHaWtwJMru5T+i7h0+pJakIAKcpSQ== Date: Thu, 8 Feb 2024 22:31:36 +0000 Message-ID: <5805637e8b03428ad79c1cd03d251f4cb41d16b6.camel@unibo.it> Accept-Language: it-IT, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: Resent-From: Claudio Sacerdoti Coen x-ms-publictraffictype: Email user-agent: Evolution 3.50.3-1 x-ms-office365-filtering-correlation-id: 4097d52e-44b5-458b-cdda-08dc28f5b63c x-ms-traffictypediagnostic: AS8PR01MB7333:EE_|AS8PR01MB7527:EE_|AS8PR01MB7333:EE_|AS8PR01MB8859:EE_ x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR01MB7333.eurprd01.prod.exchangelabs.com;PTR:;CAT:NONE;SFS:(13230031)(346002)(376002)(396003)(366004)(136003)(39860400002)(230922051799003)(1800799012)(64100799003)(186009)(451199024)(6506007)(6486002)(966005)(478600001)(41300700001)(71200400001)(86362001)(5660300002)(7416002)(2906002)(76116006)(110136005)(786003)(38070700009)(66476007)(296002)(64756008)(316002)(66946007)(66556008)(66446008)(8936002)(8676002)(6512007)(921011)(2616005)(38100700002)(26005)(66574015)(122000001)(37630700001)(36756003)(83380400001);DIR:OUT;SFP:1102; x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: u7CFxfhgcNxOt9vLJafsg4yoL1aFh9hzierp1Eaeh2H5a8zp3S3RUMyzzq6hTY00qyBdsSE9vsrFvLT3IdK7EmRMkRrK0gMk244QCZRdJkk7W6Z3wl7Im4sSj9YiY0Ogpd/JvuPV4zQJPaKg9xR+Vx3BQAAm+aMj/ZtPiMGev7aBYB3vfUKW845d5MEy+sMgoUnC7Ar6GSVD04cUkyM1Bz2Y4lxLAv50rdRG7+5JLdiVTP9i98eBIHjWJUGvctNrNBGu2vbiD4UtDmmJ0XUgeLr4kd2FtrWcOQ6CTx4m0xaVRROnSvdqOm5sB4ca9R7ty9Gc0L1ZDgadCY2lqhHzLkflOhqZbgnRmP7Zfzx0XAbSDyQ5ed/W2/39SvwgKrVrRQZnlyDJm4uPoqJGT9qWAp8sa5MUu/FLgjMi9AHXh74gK59L3nxVxdOf4xzR6nrsaP7o2SG/hSc/VPxQVGG5tLqzkD0acXI0aY/prifot+JSevBaax1fiNFTiVuzfSs0fGuqdkk28AjA60kTC3wjmklNn8W9O7kYd0xRTTX8aEo3ef2qh0ILiylv58ioPFdskYnc0a1zK8f2jvl0xCqgwm8I4rde5X5tka5z1NpadVDDmgxVApvhEFQ3Hf0PjE15 x-ms-exchange-crosstenant-network-message-id: 340ec226-6b6b-437f-52cc-08dc28f32bee x-ms-exchange-crosstenant-originalarrivaltime: 08 Feb 2024 22:13:25.8397 (UTC) x-ms-exchange-crosstenant-fromentityheader: Hosted x-ms-exchange-crosstenant-id: e99647dc-1b08-454a-bf8c-699181b389ab x-ms-exchange-crosstenant-mailboxtype: HOSTED x-ms-exchange-crosstenant-userprincipalname: XVuJdA9BuQNpFlw1CiAOXTWUmBYKV6/2FvxrNNgwuN0t+3c+zXOxeS2FHblKD3nXIZfWrld+9M2erbsJN32JDyE9I/zZ6peKEm2B6Vo+JXc= x-ms-exchange-transport-crosstenantheadersstamped: AS8PR01MB7527 x-ms-exchange-transport-endtoendlatency: 00:00:00.9619388 x-ms-exchange-processed-by-bccfoldering: 15.20.7249.038 x-microsoft-antispam-mailbox-delivery: ucf:0;jmr:0;auth:0;dest:I;ENG:(910001)(944506478)(944626604)(920097)(425001)(930097)(140003); x-ms-exchange-crosstenant-authsource: AS8PR01MB7333.eurprd01.prod.exchangelabs.com x-ms-exchange-crosstenant-authas: Internal x-ms-office365-filtering-correlation-id-prvs: 340ec226-6b6b-437f-52cc-08dc28f32bee x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?eWU2dTE0dDAveFZZSTd5K1JjSmFxS0RaNXdXa2kvK2FtVWlIVzFJMjJrNFl6?= =?utf-8?B?bUFieUN3T1FGTkVWOHZNMTJYSTZFUjluQ2FqYUVzT0Y0dmplbnJPQU1IZTd4?= =?utf-8?B?bExHRVd6SzducUprYUcrV1VjeEtTOENNbEtMakRZK3BTUGVHc2ZXRVRTZlVh?= =?utf-8?B?YTJIQlRaY2RDV292NTFFeGNaK2hvdFFiMWpuSXFKNWl5VFlLYlovZWQ5a0RE?= =?utf-8?B?N0VrN2ZNZFJqSjFTR0NDS0RHN0FtTGRuV2Y2TWJiSHk5bHhhNHN3VnMvR2Er?= =?utf-8?B?ZUpocXZuU2dNbUVVVmlBU09VYWVtcG1GajRHNGxubjVDeDVQQUk0MjdZcTZ6?= =?utf-8?B?QlhKbDM3V05WemVwKzJHNWtIYmVpejRxMVNhM2JCQXRBMlFZUmJMaFV3cU5l?= =?utf-8?B?ckFMZTZYL0pVYTU2VXF2TzJEN2h6WklqYVU0SFhBaXRzOUtMMktVMUFyWDJu?= =?utf-8?B?K3F3TW9vQ2JrQTZDbVEzTWFGeUIyajZ0ejJlWkc5d2g1WWQwYjhrTnJ0dEZE?= =?utf-8?B?Uk5nSUcxVnZJUEhvV0RXWEdDakthZHFqdWVRVnFoaUFER1Q3RnFXYXh3STE0?= =?utf-8?B?RDFaMlU2ZWUyZU5CT3J5enRpUk0xcHhwZU13amxWQTdueXA4SzZYSDZXcUdI?= =?utf-8?B?ODFqclBvSFcremlQUms3OWpLWjg0NmdqcnYxSkdZTldaN3BBVy82N05QOCtu?= =?utf-8?B?STI2MUFBOVB3YzBldUg1cjBWN2lEQVE4dmFwdmlWSmZ1dXl4NzN5N0IwNXZW?= =?utf-8?B?Rkc3WjZPZUZ1WnR1ZXFYbjMvTDlJVjJmTytibnV6UzZodGFqZlo2SHFoQUhS?= =?utf-8?B?VFg3K2tqaDlPUmVjSktXRk4wZS9md281anNBZnBPcDhjK2NMYllRQnQwekp5?= =?utf-8?B?ZDh5U2M4MEpoeUJNZWNLbjRNNjRWQ25WeWNZcTVGZERZbGlKZXM0SmxhUW9I?= =?utf-8?B?OUdFeHFSV0w4MysyTHlZcWJOTUZxSFBBRFp0U0c1RkRZSkl2OUx6elU1TzU5?= =?utf-8?B?cG9TM2JDcUtvT0FkYTBpLzcyVDc0YTNsUHZmZWVMZjhOdFVwbkRIQjBPV1Jj?= =?utf-8?B?bUpZa2RCK05RQmplWEVoL0xjdHQ2Y0NzY0VEMXJoVEhZcDhUblJEMzdTRjhB?= =?utf-8?B?aG0zQ3pvSEQ0d0VWc1hwU3I3VWI1amJRVFo0WGw1VW9UWWMzVklrZ0VBYWs5?= =?utf-8?B?Mk01WUhqbDRZYkUwZjZGQkozMlVoNnhBeVc4aDJaWDcwakZ3TnQzOUtvMm5K?= =?utf-8?B?T1RPR2NJRmFncVVwc3VZb3F3ckhSOG84alNuTG9rbUZXSWJRYVREVEhhM3BD?= =?utf-8?B?cWJLamlwK3NLS0tyczRkTjV5UDR5MmFveTB2Z2wxMXdzYVgxOGxuWFB1aFRk?= =?utf-8?B?VDZhK1N1bGV5cVNXWTN4aFpsT0JkRTEyN0Fwbzd1empORWJvcFVsU2hHTUla?= =?utf-8?B?d3gwN243N3lyS0RmOHVNNHB3WkFvOHZPUVRkczhSNWc5ZjlycUJkWWR0R2hi?= =?utf-8?B?eXVTbFhWOTFTUzFDcUNzNFJrM1VIem5sMDVlZXdwSVllaHNLYVRkN3Vpbm1K?= =?utf-8?B?bmpERHp3bXRyd1dXS0s3QjZxcVpRRkl2SmVVS082dkxOcnpNaVFpeVlNVjZN?= =?utf-8?B?d2pybTlBbFlOdDh1enB0VE41QVNXVGwycnNBWUVzSEVKTEZkOU1DQUlYNzRT?= =?utf-8?B?T1NDaExpREFWcVpFbTlJTzg5d2V3dEw0SUJWY3hvZ3phN0VKMnVJOHhXT1FX?= =?utf-8?B?UjRBRlJpQUJrT0JzODRja3g3WmN0em12RldtUWlvYlRBV3JCTWVRZXMwQXJi?= =?utf-8?B?dFJkVHZHM0xHY3BubTk1VU9oaXJWbTNrQlkvRXNIUHdza1d6VGE1MnRJcU1M?= =?utf-8?B?V3VxVEw0ZDBNdnFOSkdXM0sxNzVlMmFBamhJSFZiOUFrc2VYVzd0YjVkWXln?= =?utf-8?B?bEwweCtXalROTDYrT0l0K1ZJZmZ1dkl4Ui9MZmc3YUFvUEZ6aG1qdEVXQWVF?= =?utf-8?B?TzNYWlRmZEhkMlk2MjdLYWhGTGtsYUtXdVVoaXpxa2dZcFZmb2Z2MkJGTDR1?= =?utf-8?B?NGVJTElyOXhUL0g0OUdia3hWeHZnbE9vYnVMam1TeU5NREd3Qk4vWEZ4d2tv?= =?utf-8?B?WElKTURJRGxzbHJ1YXpzUnFPdmozSUJOY21UYzBGOVpqTjRUSnJuZWd3TDRw?= =?utf-8?Q?aGlA30ACjFT3JgqsmJdnrxA=3D?= Content-Type: text/plain; charset="UTF-8" Content-ID: <0715BFE980718F4AAAE9A6E61871B250@eurprd01.prod.exchangelabs.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: unibo.it X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: AS8PR01MB7333.eurprd01.prod.exchangelabs.com X-MS-Exchange-CrossTenant-Network-Message-Id: 4097d52e-44b5-458b-cdda-08dc28f5b63c X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Feb 2024 22:31:36.9168 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: e99647dc-1b08-454a-bf8c-699181b389ab X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: O5evdZhn+e5V4i90TKFeHBdl1yqr+W4CRsh6LxQJgGoxyCttIydopv3atu18HuELj8tBjvt1qmy7H/xLqg4SQ04dzaPc4lDqn92C+GfJdUQ= X-MS-Exchange-Transport-CrossTenantHeadersStamped: AS8PR01MB8859 X-Original-Sender: claudio.sacerdoticoen@unibo.it X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@unibo.it header.s=selector1 header.b=B+2jz9+c; arc=pass (i=1 spf=pass spfdomain=unibo.it dkim=pass dkdomain=unibo.it dmarc=pass fromdomain=unibo.it); spf=pass (google.com: domain of claudio.sacerdoticoen@unibo.it designates 2a01:111:f403:2611::700 as permitted sender) smtp.mailfrom=claudio.sacerdoticoen@unibo.it; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=unibo.it 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: , Logical Frameworks and Meta Languages: Theory and Practice (LFMTP24) https://lfmtp.github.io/lfmtp-page/workshops/2024/ =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=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D 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, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, 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 expressiveness and lucidity of the reasoning process. LFMTP 2024 will provide researchers a forum to present state-of-the-art techniques and discuss progress in areas such as the following: * Design, Analysis, Implementation, Evaluation, and Application of logical frameworks like LF, Abella, Beluga, ELPI, Hybrid, lambdaPi, or MMT * Encoding and reasoning about the theory of programming languages, logical systems, type theories, and similar formal systems * Theoretical and practical issues concerning the treatment of variable binding such as higher-order abstract syntax, nominal logic, explicit substituations, or binding signatures * Representation and reasoning about features of logics and languages like equality, inductive and co-inductive definitions, inductive types of higher dimension, universes, as well as associated reasoning techniques * Frontiers of logical frameworks such as canonical and substructural frameworks, contextual frameworks, functional programming over logical frameworks, or homotopy and cubical type theory * Logical framework-based tools and services such as theorem proving, search tools, or IDEs * Two-level languages to program and reason over logics like tactic languages, reflection, or meta-programming in interactive provers such as LTac, ELPI, MetaCoq, Isabelle, and Lean's meta-programming), including implementation and use cases =20 * Graphical languages for building proofs, applications in geometry, equational reasoning and category theory. ## Important Dates Abstract submission deadline: April 29 Paper submission deadline: May 6 Notification to authors: June 3 Final version due: June 13 Workshop: July 8 ## Submission and Proceedings We solicit regular papers of up to 15 pages (including references). These must be original and not simultaneously submitted to another venue. They will be reviewed, and we plan to publish (pre- or post-) proceedings in a series like EPTCS or similar. In addition, we encourage the submission of abstracts (1-4 pages including references) describing work-in-progress, new ideas, challenges, or other interesting informal contributions. All submitted papers should be in PDF format following the EPTCS style guidelines. Submissions should be made via easychair at https://easychair.org/conferences/?conf=3Dlfmtp24. We will investigate the possibility of having a journal special issue for extended versions of selected contributions. ## Program Committee * Florian Rabe (University of Erlangen-Nuremberg), co-chair * Claudio Sacerdoti Coen (University of Bologna), co-chair * Mauricio Ayala-Rinc=C3=B3n (University of Brasilia) * Mario Carneiro (Carnegie Mellon University) * Kaustuv Chaudhuri (=C3=89cole Polytechnique Paris) * Cyril Cohen (Inria Sophia Antipolis) * Theo Winterhalter (Inria Saclay) * Other members TBA=09 --=20 Prof. Claudio Sacerdoti Coen Department of Computer Science and Engineering Coordinator of the Undergraduate and Graduate Programmes in Computer Science University of Bologna --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/5805637e8b03428ad79c1cd03d251f4cb41d16b6.camel%40unibo.i= t.