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,URIBL_SBL_A autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-qv1-xf3c.google.com (mail-qv1-xf3c.google.com [IPv6:2607:f8b0:4864:20::f3c]) by inbox.vuxu.org (Postfix) with ESMTP id 7115B23D18 for ; Mon, 29 Apr 2024 17:02:51 +0200 (CEST) Received: by mail-qv1-xf3c.google.com with SMTP id 6a1803df08f44-6993edda019sf67189416d6.3 for ; Mon, 29 Apr 2024 08:02:51 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1714402970; cv=pass; d=google.com; s=arc-20160816; b=iOrd9AAbJ8PkVU1y8/sCqoJk0MJ6Q8wyO2Xmz87Al0xzvcBgj/BKEoB4dJbFv68fE7 IfQoSCQnChGC99rFq0NQ0v5vG/uwYU+9ZGVZSTRciBK9+LNiXHGey11L3xNGcYFxaNB5 z0W7V0TcJCAJC3hXwtbspzAAYYlsbpMfa20IeiyjBJCjv+K3/VVp3BBidNp0UwlCLSc9 4kSECMlHZpwKQLywoiosr494wWgay08uSLVsDDi5jtu6UbTagUWjFlhdAoeNw/zhlpB8 TK5viMqFGFSSUP8ILpyKs4xC8SPuV1OMwUrEk8K99H1zVv9x0KOMx72v1MbCREyvobxs 7/qQ== 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=HIOfWdiwYYka36kOsjGhN1RnAKMB4IITjutr2gKYGB4=; fh=1gCtxgaMZj5qIUPRKHrWz3z+MSLL3KPgXJ1Aibe2QY0=; b=0j+ptGJ8AixdlbETh3tXzDSbizTV1fnOhkgeZedAbqDaKTfi2Ax09UkzuyltgbJ7Lo 4h88n1euyOnsgqkw7v930Y1hbWY7c3b/uZJG22pgUK4/sUsL0nEZR2q5pTuCSqGAw8OJ KiJ6phef9QaZyypexJDBVOcghQ+0fxqVvN7tu1m325jAt8P7enUyQ1XvdlAurzv4Mvph OdkAIo2W3sJMplOd79UE5aJnUDv4La9fZrc1sExqKufwmq3HIZM36TpxwmKK8jrqArvt CKAjnWsngZ5Z0yEV8ZASpNDQAKZmOALU33kvMKpNwqLrUwNi8ZPE8urjGUQHUT4OsSM/ YlhA==; darn=inbox.vuxu.org ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@unibo.it header.s=selector1 header.b=M1cxEjrP; 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:2613::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=1714402970; x=1715007770; 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=HIOfWdiwYYka36kOsjGhN1RnAKMB4IITjutr2gKYGB4=; b=Uz0dzX/H/WuS2f56QeNkRSZGLXdx5Nz49M2CCUzFfZ+rHr7t+9s2G9GHKs8n2tvBYP xfrDpRtgSXCXOTNi2UVgPkURAgXjYf9f0aSx5pCfXKfK3BNkdVtSke0gfv+slgk2qxWb blTtLEltdBUYSKI8VvJc22Bme0s8vRDHinczUX04J2xWdon0XyJPa3XjDLtVhI/xS9mW mV2+pPdmb0sbdbRZu7g1V7GZ3F1rekL2pC21BERQz8m+ZTTVg2eSDuaBH3guvziM95hH BvJhPy85YC5EOkVR0dY1HGnHGv57eApLXsYQ0q1ngNvk/kGrMf8EZB3AoT7vBQ/zbAi5 Oe1A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1714402970; x=1715007770; 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=HIOfWdiwYYka36kOsjGhN1RnAKMB4IITjutr2gKYGB4=; b=FIZ64TjmLZx0q1zvmjKaOefJVlcqJYPVnvIcf6huviPP9QKvVzA6PC+rfAZ+1eYpEQ imNduYbfFl0P3ybhIwvWXht7hbPciRMQ42mk2EfEdSEo0Pq4vX3Y0cCmVBLqmqjROGof Zthh6eV5ayRqug3R8q8GVunIis1vGPD89pOAO5fe9hGy3G43Ft/AtQa9sVV+Hjaek5S2 WyEcZBDBFaxMdrQlDBz82U5kHd1tLrHQLQXl9IUBRubCuCh8vvesVL121zbX53Te+L34 NRY0i5rYuwMQCG7bW4/2GZPFC/IY5ihdJwunm2YOty8Le0lYmsJ1U9fsjz59qb6KZ/Lk eg6A== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=3; AJvYcCVg6Ba6dsnOvPOHe+16nzQxtgs+YoPl3ghDWVmvsM3yt/FXAQMh8GaUUd34dWKrCHtby59hdrUikIrcvRnkNXmeSA== X-Gm-Message-State: AOJu0YyoU5pJgT0Ce/1aPu2o4rIN/2A9Ke5gJSc5tDeVjZh1aiWw51Cj OvFEKmZWEBRG9hkfVa/y+rE84EVNedw6k2wjdzadaffgPTF/vOho X-Google-Smtp-Source: AGHT+IE7ecdtwdjmrtGq8mT758Xaz1XM37/P69EQSjRXG3vorfBxkSYuN72zq/b3/T3pj8BcZ2wIPQ== X-Received: by 2002:ad4:4ee5:0:b0:6a0:43c3:944c with SMTP id dv5-20020ad44ee5000000b006a043c3944cmr16703972qvb.15.1714402969732; Mon, 29 Apr 2024 08:02:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6214:400d:b0:6a0:cc6b:195f with SMTP id 6a1803df08f44-6a0cc6b1b29ls18385126d6.0.-pod-prod-02-us; Mon, 29 Apr 2024 08:02:47 -0700 (PDT) X-Received: by 2002:a05:6214:250c:b0:6a0:76b9:3e11 with SMTP id gf12-20020a056214250c00b006a076b93e11mr15523106qvb.53.1714402967365; Mon, 29 Apr 2024 08:02:47 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1714402967; cv=pass; d=google.com; s=arc-20160816; b=oOfwOzJRnOOSEOr92FYHk3H8vmYOrGr9wQZGYpBaGeD4pTGgz+d4iDboZ5n7V/OmGE KBB828KI/mhMyGm7FbXW1PyTERxqUpzSbcR5LRbW7Cnhv6TtAGEAh2U35Jmv0KSPhsEg lhyZX9jqeKv4/h+3f4Tw2VSFQOGpkRMI99Q/zmEu6AuG2+RunFFBUrhBR/L923o9yACR CLe7Ow1if20iLu1FZwCkPn5x7Jy+i6oHzkcWjImxm3fedyEMYYTEale8u94t/L7MZ50n CMXc2eI8C0bsoTdQ7ftBmjNpWg42XTuuzedHMyoBMZ8FG8ldNPlzvJcZGTXhFVo/iouU uzWw== 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=6+MvaEeisRAXJs+30JZuQWGY4jiA6oCGa3c9CClZT5c=; fh=3Ym9f7wuISLb1x3fB7UFAuBdmVezHj32enpHypcmrC0=; b=cL6saHqPDI3Qey3qzmuhHLly5cqaJw1IvUEWmZjaHsAV93yu6Dhwpd/Rs02dZf2JHN UipbFlUssQGaIB77lIYRFmYS4HL7GBx5ZqJQ3KKIV/Jyr8G+1X0OUHf7jhDuIdlKTiMs dzxRbN8WyDwk0jfbOUF7/WSxgZ4vzvabmGJZ3zVagMwzeXBW6LoLh4xaXnt8qdOXzPwL Ef4XhCDMqXWEGqqo8RIjABsZZVjddPkp2+92iUpZKhBooi8ONCrYKPUFhwaGAjalcPpU l5OSr2whQl/ITLvxtzhOveNBQaq+sf6vii8D33xxewfnbGc0ras9WbJGrz06RIpuGMnH d4/g==; dara=google.com ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@unibo.it header.s=selector1 header.b=M1cxEjrP; 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:2613::700 as permitted sender) smtp.mailfrom=claudio.sacerdoticoen@unibo.it; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=unibo.it Received: from EUR05-VI1-obe.outbound.protection.outlook.com (mail-vi1eur05on20700.outbound.protection.outlook.com. [2a01:111:f403:2613::700]) by gmr-mx.google.com with ESMTPS id g8-20020a0562140ac800b0069b43ef64eesi1609926qvi.0.2024.04.29.08.02.47 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 29 Apr 2024 08:02:47 -0700 (PDT) Received-SPF: pass (google.com: domain of claudio.sacerdoticoen@unibo.it designates 2a01:111:f403:2613::700 as permitted sender) client-ip=2a01:111:f403:2613::700; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=PP+Y50xysRfFMOEaLrm+fkqIaCvcLKTnRJMPwzpR/yO8QfHlWUAcyJfFJUU5N4bw+nGMvyD3HWzNBs/5WkICpkNnOYB34zpgc4mtpye714b9P6SXCQyRYqxStS4MYaVz/9g9TDHIPUvTtjxwyelPlaYYWTyrN1XcDNRQGFODQ59IeCPpPZFET32GGy8CuxuQhfCFEV6V5pVb/hFesET5ItaFlagP4H2Wtsgou+Hm3Jjg2dtkTtERj4nWo+pkLyNsmZre78zgX7KglOTAvH/VIffV7155bclEUg3i/+KOMjoCdLoULX+Gamg5M+jBz7gF/fZuZ0tSIlFuW+8SOUpeDQ== 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=6+MvaEeisRAXJs+30JZuQWGY4jiA6oCGa3c9CClZT5c=; b=mDzLb3mXifNG0kSLwjDfeYmlGxgSrEGaxtk9YXRNR94IA8YGXrHzzx8M7iEcurKg+BIXY5mEXxymifmvT1zbXiGHtaWL/R4J6dpJ3BncaDbrxjvzG3RGnmu6ZHCzkwae6xmp34F7Pn0ylgR0zuFu9F40J9UkugL20V3YwVt4kdvJKP4VmCGeKZSBt7ORty33D/5PmL0R/NzxWlDS2GBg0w0l00xW6P7Act9iRVcQS69N4Fh4ndiUBoyK4fiEzLZJ4LSG3QX9qYfMrMvSweazkwMUUs5oYmciF4R/hcqBS3/Dq/TeZUYAYDH50hC4GZM9Jx7eDkUIqc/gpPRMtxaoWA== 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 PAXPR01MB8204.eurprd01.prod.exchangelabs.com (2603:10a6:102:200::6) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.7519.34; Mon, 29 Apr 2024 15:02:45 +0000 Received: from AS8PR01MB7333.eurprd01.prod.exchangelabs.com ([fe80::6ccb:c4bf:e6fc:dd7]) by AS8PR01MB7333.eurprd01.prod.exchangelabs.com ([fe80::6ccb:c4bf:e6fc:dd7%4]) with mapi id 15.20.7519.031; Mon, 29 Apr 2024 15:02:45 +0000 From: Claudio Sacerdoti Coen To: "homotopytypetheory@googlegroups.com" Subject: [HoTT] Deadline Extension: Logical Frameworks and Meta Languages: Theory and Practice (LFMTP24) Thread-Topic: Deadline Extension: Logical Frameworks and Meta Languages: Theory and Practice (LFMTP24) Thread-Index: AQHamkRxtrYnEjmuKka4COfJyBFf0g== Date: Mon, 29 Apr 2024 15:02:45 +0000 Message-ID: <7c584534625873ecd1aab6bf69335103f6b715c4.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+b1 x-ms-office365-filtering-correlation-id: 35c8ed6a-88dc-41b9-ecb8-08dc685d6d19 x-ms-traffictypediagnostic: AS8PR01MB7333:EE_|PR3PR01MB6892:EE_|AS8PR01MB7333:EE_|PAXPR01MB8204: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)(1800799015)(35042699010)(376005)(366007)(38070700009);DIR:OUT;SFP:1102; x-microsoft-antispam: BCL:0;ARA:13230031|1800799015|35042699010|376005|366007|38070700009; x-microsoft-antispam-message-info: =?utf-8?B?bVIvdGVLT1M1amlkOGNUTGc1Z0JrcjBxa2ZpbUdncWk4d1JqV0xKNWJ2WEE0?= =?utf-8?B?Z1FXUFdFWFI1cGdFd2xxczdxUnpEVlJ2eVIrUzJLZFFkb3JsOU9lNmprSlEx?= =?utf-8?B?VVF0eWtHTmN2dTZSazZYVHVjRVN1RHRveTVNdHJ4ZFRMZ2p0QlQ4VWVuZmd5?= =?utf-8?B?SnN1bGR5VlNxcEZxd1diZnkrU1c1MUhveUYxUXVxZmMrYU4yd29pNmUxTjV0?= =?utf-8?B?UitMN1ZuNlNlZ0NWd2g5bloyT3UwendhdSt4WElhTUFXRFRERkwzdURnWWpz?= =?utf-8?B?b1UrMUNkZ0tDUTJKWkc5clFDQ2U2L0l1dUpxeUNtcUdUUkJWVWxXUVN2bDNZ?= =?utf-8?B?TlgzNS9OUnFNYm9PNm8xRlJqMU4xbW0vU0xlbFMwY2pMUzd6THBwWTBVWDdX?= =?utf-8?B?SFVaVlpEZmg5OXhNb1ZERWlucTNnaEZBeUtuZGl6a2M5SEZya1dQWWdzN0xF?= =?utf-8?B?MVU1US84YkNvYllLYTZDR0hzN2p1em0xb1hDZ3hia2U5M2FkblZkTEkzOWhW?= =?utf-8?B?cmFBRDh6WFZyWmxaTEZZWlRvLzdXZFM0TG94c1ptdU1WTDRuTnh3UnhHbGVI?= =?utf-8?B?aE52NjFtNExrTmZUQmZYRkZHa1RCYklFblJYM1ZHeVZuYjgraGwxZFVjcW94?= =?utf-8?B?T1paWGQxeVJrMjluZklvU2xqKy9wOFRFZU04ZHVWOGhzK3BaSTBJbUdLQnRr?= =?utf-8?B?K2NJRjIxcWZIOUtuTFM4TEp0VWRLaUFPbVdlM2ZlalR0OXZabmpRY3VCQlY0?= =?utf-8?B?UE1OSGd5Qy9KcVVrMUJVRm42NCt2N2pXc3ArdHRlS0NFQmNYR1ZkWTZGMENw?= =?utf-8?B?WWhkbmp2WXo1Tm1ndUZBRWV0MS8yMWVDb0M1WFkycEpQMzkxZU1lMEVnYWVO?= =?utf-8?B?eW1rOW5yYjZXdU91SFk3QS9Xb1VsUGVBZHJGN1VoSU1xQXg0MXl1dVFNamdP?= =?utf-8?B?d2NqRm5uUTM3WlpFU093UHpUY0RYOTlmRVdMaERTM2YreDIvc3F4ODdaQjNp?= =?utf-8?B?Zkl6dEh4cWZ6NGlJclpZZGlqR0p0QmVDWUZTVDN5YjIyWWxNYlVRTGZUUU1T?= =?utf-8?B?eWxpbk11RTMzUm0zb2lONUVhc05vNHNRaVE1YW9KY2hocklHUUxET3F3cTFT?= =?utf-8?B?ZUpqWklmUHZSdjgwb1VoWFliU2Z2a2tmdXJiZWwyVUxLdDRYZEw5WWwzMkxl?= =?utf-8?B?VlBPMGh4SVYzVzl6Q2RUK1ZwaEQ0ajlqWjQyQ3VEUzB2bVB4QnhvOTVOTTZO?= =?utf-8?B?clZpdzJqU2I2emxsTDBTNnBWSCt2YWZoMU4wdVpNaGlsbHEwdnUxMk00NHFs?= =?utf-8?B?WEhoRmxBMjJFaXNhb0RDQWpPalFTc3pidXp2bmkzZFdPd3UrR2FnQWJ3WnFa?= =?utf-8?B?SEZ2Q2Nac3lieTQvSExBc3lML3hIQVQ2U3pHSDd4b2lZUGxQMGVnNDgwWTU4?= =?utf-8?B?emI3TTBIQjNXR3F1SkZKVTQ2S3RUeGN2aWN2K0xqV1RLRVoxV1RGK05qZzA4?= =?utf-8?B?SjZUanlaenFuNjVEMWdMYlUwZ2VwTjNqSGp1OS9HeUZVNUJxTHd0dzFYKzRP?= =?utf-8?B?ZE5BeUd4SHZoQmdkWVduMkdEQW1BVnJQUjExc2E3MUE3OGNTUTBDQ0FyaWh2?= =?utf-8?B?TGgzYXRFaXgxb1BxaHQrNDY0ZkZRWHdaMEtmODRzRk9pSTB6SCtCVjhBRDFn?= =?utf-8?B?V1AxS1U3czJPbmxyQU1Ha2NLNldUMDh5T243c1lKdUFJaUJkSllXRHZnPT0=?= x-ms-exchange-crosstenant-network-message-id: 8ae79923-ea15-4269-d845-08dc685b93e1 x-ms-exchange-crosstenant-originalarrivaltime: 29 Apr 2024 14:49:31.1889 (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: GANBT8ojDMXKXRrQaGniVRwlA5xMG7FXRmq72TfuURDaonRsSKNSPUYJCqIQoh92sQA4J68vIr9IKpLDOVTAc2PwkuwJ4y405GSqjnZDroE= x-ms-exchange-transport-crosstenantheadersstamped: PR3PR01MB6892 x-ms-exchange-transport-endtoendlatency: 00:00:00.8093707 x-ms-exchange-processed-by-bccfoldering: 15.20.7519.031 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: 8ae79923-ea15-4269-d845-08dc685b93e1 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?NFczVW5vdm52dWx1b0g4dmdhNC9EMit6NWVJcGFPNENEQUFnOStZNVhJRXdQ?= =?utf-8?B?Nkh1Q0VUTitFRUZjUnZZR3JGZTcrdkZ4NGx6eXlVNERST01BeldOS1YraGhO?= =?utf-8?B?aWtyUVBsMXFEWEFYRUZxRExpRHU2dmtUWmVtamIxdXhlR2FCb2d4MnpXSW8z?= =?utf-8?B?aXVSMEE2S3k0bmdoeUlENG8yZDRwRlZ2RGM2TFJtcGNTU2JnNFhNcFpPYmN4?= =?utf-8?B?MkJuakZwdWFxTk1YOEJJUXhlNVBpUHFFRFhqc3BzaDhrcTJ4MHZaTVd3d2U3?= =?utf-8?B?ZEVLVVNwTTg1N1ZJL3ZWazBBSllzMFQzZHE0eXJKQ0dJVzRqL2Z1ZXJaZ1pS?= =?utf-8?B?L1hyVFJLZVBXeUlGVGJsV01MRmo2eDBEWFVYbGhROHBMUENUb2FOQWRFY1Bw?= =?utf-8?B?QjBnRmhUbEhFVGJkTStDeTNUV2dkVy90N0dNSnZnRUpLUStxUXNxUmhXWnF1?= =?utf-8?B?MzU4Z0k2RThvdFE3bUxMN25rSFY3RGJmWUtmY1lvRHpYWmpjYWMzYnI1U1V6?= =?utf-8?B?dXdwYkpha3pOdUtHTGcrUkVHQnJabWhuMkNLYTdSdklTK09STjc2MG1VRzVO?= =?utf-8?B?RElVQzBLTTZ4UWFGZFdSR0YzUXlneUpwQkZ0bDNqRmEzNHJLVzA4bEo0U0Vh?= =?utf-8?B?aVgwNkllbUlTNmNuSXZjTjZVYXYyR01WUStlUzZBSHBqMmxOVjkxQnh6NUNB?= =?utf-8?B?Qmx2Y0lsQ1ErZHdXUTZpS0hsaFJSRDlsVzl4WjVOUW4wY1RhZFpNWW9XUlkw?= =?utf-8?B?a0dBdU9RSjdkRVczWU45WU5ZUFJlRHBrUGNqTEplUHBBdUdmVm9YSU9vQ2g0?= =?utf-8?B?bE9jYWNpRWsvMHBkZSt2T0F1dGZCM242NnZDL2tQc3JsWHV4RSt2dkNhMU9V?= =?utf-8?B?YXZqR3UvRWgwVHlUVjNYa2hDR3AzRDRyMThEclNjSDZBNWNNR0Vuak50bTdk?= =?utf-8?B?bHhmczN4V1I2NEtSTy9UYTA1VEFxeVJsdGVaWHMxeHNCaVRCdkQ3eE00Z2dr?= =?utf-8?B?dG9HRmNMQmFCTDRyK1RBRlFGTnducE1VdmpCY3V2bXVxYnRxQVMyM09EdU1L?= =?utf-8?B?eFhnSDJoVGpTdVJSTFlhZ1lNb28vajZra1dzNjhMU0Y5bURTcmJqMXhQZzd4?= =?utf-8?B?Lys4ckZ3U0RMS3A1YW8vQjdudHpDRHltY1c1K3BZY3cyQ3FkQWVRUkpMdHNP?= =?utf-8?B?MmhjcTJWZ0JvYVNNdEdEaXArU1E3a1YxMkpZazhNWEFuWmIyNEhhZkNIYmd6?= =?utf-8?B?VnZ1UWN1ZFpLVUVoK2JGVmhkQUpITVFsaU41aDhOUWFHY2NjQ3VUQXFVdW9y?= =?utf-8?B?S1pQSVE4TklPMWp6L29xK3l2YzhOcTRkYmRGS0ROSjJHSDJndk5lb3BPWktP?= =?utf-8?B?SElodFhURkpCWVBTaXE4RWp3UWg0WUxoZWJ2NHlzSk94akcveGhpNVJ4eWxw?= =?utf-8?B?LzJVcDhqV1VDcXo1dEg5VGlNSVp2eG96cGduZEM2R21YcGxwbWhpUjFvbU9p?= =?utf-8?B?dmVNSUw5V3REVjVmTGVCR1RxUWJsSXlwaldFQ2VVOXJweVc0ajh6Z2JPelh1?= =?utf-8?B?Z0JOU0g0c25yU3B2bEl6WVBjVEVNOHVCL0pEMFErOG9KdFNYd2VmN2RKNDht?= =?utf-8?B?aHVYU2NaV2lFTjU2aFltU1czbFV2YjcxMTZLbWc3aGU5VmJTTUhaUXZ0enVL?= =?utf-8?B?ejYxNkhRa0FXWGFmZzVkK05UUnpJRVRqMUxEOENYQzRuNGZLcTRkeHZBOEpP?= =?utf-8?B?YWNKTlBRRGY3bE4xcXFPNGhZRUxJY2UydWNlWThFM2Y4eC9JSHRrTXNTckdm?= =?utf-8?B?cHBjY2V0SkNFTEM2RFByd1dHWm8vVEpkNEtvOXNDWWZLdXN2S1kyUDd1Y0JJ?= =?utf-8?B?R1hxUWY4SXpSV2FRTTNWYXFXSW5ObzYyZi9YQnZHK2dpSHFkcUoyMUdPQkNX?= =?utf-8?B?Q1NsbmtxQmpGRUJHU0R3MVBzVzZTM2tKcUVteTdrSWhWMHRWK3dNZzJmRDdL?= =?utf-8?B?T1dHZmZIUG8vZDlXK2U2QVpScEhsM1ArSnlDTnZOSHQrTHU5dVBERmhEY054?= =?utf-8?B?US9mRHNHZG5lbDhvakJuWllmUWo4OSsyV0FLZUdSOElDUjZkNWN6SklFczlp?= =?utf-8?B?N0dlYmJML2UyZ1FHNE9xYUxyU0tFdTBoY3krK2I3ZG9hWUVHYVZzMkxlSVlE?= =?utf-8?B?c2pyMXh4Mkl6RUVnRFhvRDJTaUt3RHZDc0ZqaFAxRmdkczM1RFJLQnNQWFgx?= =?utf-8?Q?OLENqppge5/gtoBFdctWf1F5T+gGP17uw7oZ2KO7/M=3D?= Content-Type: text/plain; charset="UTF-8" Content-ID: <76E586AB6BCA58448EF5B872BB30567E@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: 35c8ed6a-88dc-41b9-ecb8-08dc685d6d19 X-MS-Exchange-CrossTenant-originalarrivaltime: 29 Apr 2024 15:02:45.1115 (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: tk1RxQ/F74G+XcpXdats3Nw+NkTk5XIH83v/YlH2hesMaLkij2zUwWCxb79fCchc4/OvbXJeYbNpRpsjwwQpha3Mi7l2rIWjR4oXYKj2aKw= X-MS-Exchange-Transport-CrossTenantHeadersStamped: PAXPR01MB8204 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=M1cxEjrP; 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:2613::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: , Notice: due to multiple requests, the deadlines for LFMTP24 have been extended as follow: * abstract submission: May=C2=A0 6 * paper submission:=C2=A0=C2=A0=C2=A0 May 13 Here is the updated CfP. =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 =C2=A0=C2=A0 Logical Frameworks and Meta Languages: Theory and Practice =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 (LFMTP24) =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 https://lfmtp.github.io/lfmtp-page/wor= kshops/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, =C2=A0 logical systems, type theories, and similar formal systems * Theoretical and practical issues concerning the treatment of variable =C2=A0 binding such as higher-order abstract syntax, nominal logic, explici= t 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 =C2=A0 * Graphical languages for building proofs, applications in geometry, equational reasoning and category theory. ## Important Dates Abstract submission deadline: April 29 EXTENDED TO May=C2=A0 6 Paper submission deadline:=C2=A0=C2=A0=C2=A0 May=C2=A0=C2=A0=C2=A0 6 EXTEND= ED TO May 13 Notification to authors:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 June=C2=A0=C2=A0 3 Final version due:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0 June=C2=A0 13 Workshop:=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 July=C2=A0=C2=A0 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) --=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/7c584534625873ecd1aab6bf69335103f6b715c4.camel%40unibo.i= t.