From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Authentication-Results: plum.tunbury.org; dkim=pass (1024-bit key; unprotected) header.d=inria.fr header.i=@inria.fr header.a=rsa-sha256 header.s=dc header.b=LEU8+6zY; dkim-atps=neutral Received-SPF: Pass (mailfrom) identity=mailfrom; client-ip=192.134.164.83; helo=mail2-relais-roc.national.inria.fr; envelope-from=caml-list-owner@inria.fr; receiver=tunbury.org Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by plum.tunbury.org (Postfix) with ESMTP id A3414400A6 for ; Tue, 20 Jan 2026 20:07:15 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=inria.fr; s=dc; h=to:date:message-id:from:subject:reply-to:sender:list-id: list-help:list-subscribe:list-unsubscribe:list-post: list-owner:list-archive; bh=8Qqw4nm6hw1PG2EjRz8TSeLE7th1+07yO9jRbZOasi0=; b=LEU8+6zYlb7JnuK6FRYtEW0USFydtZuz10oKTSRbYYErLDh96JcTZAIZ sct1Tnt0zE1/dOGZT9rzqJv7a7umsdf899lk5aL9f5sXCHWJR8zP3WYnX DuRr22b+jD3huYSR9SVUpwMgb9D2uSa53yh3N4fw6w7HNFsAoMYN4QlRW o=; X-CSE-ConnectionGUID: xc6swcaRTZafDy38GwcjKQ== X-CSE-MsgGUID: ar25QFI3Swueajqwsyhllw== Authentication-Results: mail2-relais-roc.national.inria.fr; dkim=none (message not signed) header.i=none; spf=SoftFail smtp.mailfrom=caml-list-owner@inria.fr; spf=None smtp.helo=postmaster@prod-sympa-app.inria.fr Received-SPF: SoftFail (mail2-relais-roc.national.inria.fr: domain of caml-list-owner@inria.fr is inclined to not designate 128.93.162.27 as permitted sender) identity=mailfrom; client-ip=128.93.162.27; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="caml-list-owner@inria.fr"; x-conformance=spf_only; x-record-type="v=spf1"; x-record-text="v=spf1 include:mailout.safebrands.com a:basic-mail.safebrands.com a:basic-mail01.safebrands.com a:basic-mail02.safebrands.com ip4:128.93.142.0/24 ip4:192.134.164.0/24 ip4:128.93.162.160 ip4:128.93.162.3 ip4:128.93.162.88 ip4:89.107.174.7 mx ~all" Received-SPF: None (mail2-relais-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@prod-sympa-app.inria.fr) identity=helo; client-ip=128.93.162.27; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="postmaster@prod-sympa-app.inria.fr"; x-conformance=spf_only X-IronPort-AV: E=Sophos;i="6.21,241,1763420400"; d="scan'";a="259539004" Received: from prod-sympa-app.inria.fr ([128.93.162.27]) by mail2-relais-roc.national.inria.fr with ESMTP; 20 Jan 2026 21:07:15 +0100 Received: by prod-sympa-app.inria.fr (Postfix, from userid 990) id 108FD83BFE; Tue, 20 Jan 2026 21:07:15 +0100 (CET) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by prod-sympa-app.inria.fr (Postfix) with ESMTP id 2DFE983BD5 for ; Tue, 20 Jan 2026 21:02:42 +0100 (CET) X-CSE-ConnectionGUID: qW5XrlDTQS2m5o9NJjoAZA== X-CSE-MsgGUID: Ru7VqIzBQ1OVlUUlE86PWA== IronPort-SDR: 696fdf61_Aii1F0R9dmqdDw+dwCRRJeXsQjAj5Yt030iczuVbY3zfHep BK05iJ78QsRzY9owN81lWfw/dNQpzNBVRSdAN+w== X-ThreatScanner-Verdict: Negative X-IPAS-Result: =?us-ascii?q?A0HrBQAJ329p/wZZH8BaglmCQYEHXjEDBAuOHIh5n10/B?= =?us-ascii?q?gkBAwENPRQEAQEDAQOSBB8HAQQzBg4BAgQBAQEBAwIDAQEBAQEBAQEBDQEBB?= =?us-ascii?q?QEBAQIBAQIEBgECgQoThk8NgluBLGMBBwI3AgEBAQEBAQEBAQEBAQEBAQEBA?= =?us-ascii?q?QEBAQETAg00KmR3MAIeMYMWgnMDEZ9WkFuBAd4nCSSBUwaBTY5CAYJJgnGCD?= =?us-ascii?q?YQOg1AEgTV2g0iCLwSDMIJZA5E3gWYDWSwBVRMXCwcFgWYDgQZuMh2BIz4Xg?= =?us-ascii?q?QobBwWBIoI8hkgPiyUDC209NxQbkEtHgieBICFPAU0XgRYtpSmfUIE+kESVO?= =?us-ascii?q?gRJqmuZBosmgmOVZA8EhUGBfieBWXKDNk4DGQ+XNMMnKG4CBwsBAQMJkWo0g?= =?us-ascii?q?UsBAQ?= IronPort-PHdr: A9a23:n0+l5R9DY/dEu/9uWQ+2ngc9DxPPW53KNwIYoqAql6hJOvz6uci5Y AqHvb400AaSBc3y0LFttan/i+jYQ2sO4JKM4jgpUadncFsor/tTtCEbRPC/NEvgMfTxZDY7F skRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiTSybL9oM Bm6sQrdutQZjId/JKs91gbCr2dVdehR2W5nKlWfkgrm6Myt5pBj6SNQu/wg985ET6r3erkzQ KJbAjo7LW07/dXnuxbbQwSA/3cRTGoYnAdQDwfK8B/1UJHxsjDntuVmwymVIdf2TbEvVju86 apgVQLlhz0GNz4992HXl9BwgadGqx+vuxBz34jZa5yTOfFjfK3SYMkaSHJcUMhPWSNPDICyY YsUAuYdIepUs5Xxq0cUoBeiAwSnGePhyiVPhn/zxaA63PouEQbI3AwuBN8BrG/UoM/wNKcTS ++1yajIwS/dYPxLxDfw7pXDfR89r/+WR71wbdbRxlc1FwPDllidqZDoMy2b2OgTs2aX8e5tW PyxhmAnqwx/rCWiy9oyhoTHm48Y1E3J+Tl2zYspO9G1VE92b9GnHZVety+WK4t7T8U/SG9mv yY6z6cJuZ+9fCUS1pso3QXfavybfIiI+B3jVfyRLS1/hHJ/d7Kznxiy8UynyuLgSMW50UxGr i1fktnDsH0Gyh/d6tCfR/dg+kqtxyyD2g7O5u1eIk05kbDXJp8nz7UtjJQcq17DETXzmEjuj K+ZaEEk+u+w5uv9eLXmo56cN5Roig7gKKshh9azDvgkPQgVRWSb/OW826fm/U34WrlFkOA5k rTBvJDbI8QUuLK5DhdI3osn9RqzFTmr3MkCkXQEKF9JYhOKg5DsO17UIfD4Cfm/g06rkDdu3 /3GMaPuApLDLnjNi7ruYa1951RZyAoy199f4pNUBqsfL/3uR0/9rMbYAQMhMwyo3+bnD81w2 Z8EVmKKBq+VKafSsV6T5uIzOOSMf48UuDPlK/c//fLujHk5mUUcfaazx5cXZmq4EuxgI0qCe XXsmMsOEX8WvgoiS+znkECOXSZcZ3msWKIy5Ss1BZqoAoneXoytmqKO3Dm4EJNMfm1JEEqME XLpd4WfR/cDdjidLdJ7njMYTritUYoh1RC0uw//yrprNPTb9TAFtZ77ydd15OzTlRQq+DJsA MqS3X+DQX1ok20OXzM5waV/rlZnylifyaV2m+VWG8Rc6f9RSQc6LZDcwvRgBd3uRwzPY8+FS E2+QtWoGT4xTsw+w9sJY0tlA9uslwjN0SX5S4MSwuiADZkwt6bdxGTZJsBnyn+A2rN33Hc8R c4aOmChiKBX/BOVAo/AlkTfmqq3JvdU5zLE6GrWlTnGh0pfSgMlCc0tPFgab0rS9pHi41/aC qSpEfIhOxdAzsiLLu1LbMfohBNIXqSrI8zQNkS2nWr4HhOU3vWUdoO/dGga0iv1A1NClgEa+ HfAOAQjVW+6u2yLNDV1Dhr0Zl/0t+x3qXe1VEgxmg6HaENv/7GuvBsUjPmdDf4fw+FMoz8v/ hNzGlv1xNfKE5yAqg5mKb1bes846Uxb2HjxvhZ4P4e8IqluwFUVaEJyvkrr1lN6BpgofdECi nQswUIyLKuZ1AgEbDaExdXrPaWRLGDu/RepYqqQ21fE0d/Q9L1doPI/407uug2kDC9Auz1uz sVV3n2A557LEBtaUJT/VVwy/gR7oLeSazc05ofd33lheaeutTqK19UsDeojghGuGrUXeKyJE wH8O8YBQc2vIekr3VWlc1NMPexf8rI1I9Lzb+GPi+agOOdtmi7jjHwSudEnlBnVsXotDLCbu vRNi+uV1QaGSTrm2VKos8Ss3JtBeSlXBW2njy7tGI9WYKR2O4cNE2anZcOtlbAcz9bgXWBV8 Fm7ChYIwsisLFCdYlvz0yVbzgISoHWimG21wyE+wFRL5uKPmTfDxejvbk9NNWNMSmdKhkyqJ Im9itFcUUS1JVthhF6u4kD0wLJeraJ0IjzIQEtGSCPxKnlrTqq6srfqj9dn0Jozqm0XVe29Z QvfUbvhu14B1DulGWJCxTc9fjXsu5PjnhU8hnjPZHp0qXPYf4l3y3K9rJTTSPlf0BINX299i DDSBx6xM8Th8diPlpjFu/yzTCr4B8cVKnCtndLG6mOy/iVyDAe6nuyvl9GCc0ByyiL929RwF G3JoBv6foj3xvG/OONjcFNvAQy04M57F4di14oo0chBgz5B39PFrDxZwgKReZ1B1KnzbWQAX 2sOyt/Ru03+3VF7a2mO38T/X2mcxc1oY5+7ZHkX02Qz9ZMvau/c4bpakC9yulf9oxjWZK03k Toax/UG42VchuAAvQtrwymASON3fwEQLWn3mhKE4srr5qpaY2ihWbOrkk9/lNWgSryOv0sPE Ga8cZAkEyhq68x5O1+Zy3z/5Lbvf9zIZM4SvBmZwHKix6BFbYg8nf0QiW97KHrw6Dc7nvUjg 0Ukjtmq+ZKKIGJ38OelDw5EY3frMtgL9GiI7+4Wn97Kjdn+RNM6Q3NbDd2wCqj0WDMK6aa+b VfISWJl7CzHX+OGVQ6Z40N7o3+dJIuzOTeYI34WydgkTx6YQS4XyBYdWDFw9nIgPiatwsGpM EJw5zRKo0X9tgMJ0eVwcR/2TmbYog6sLDYyUpmWahRMvElE4A/OPMqS4/gWfWkQ94C9rAGLN m2QZhhZRWAPVEueAln/P76ordDe+umcD+C6IrPAe7KL4eBZUv6Jw9qo3O4Et36UMd6TO3B5E /Ah8kNZWHFiB8nQl3MEQDdRkiPEas/dqRuhu2V2os257PX3SVfv6I+IWN4weZ1k/xG7h7vGN vbF3Xcjb20BkMNdgyGbrdpXlEQfgCxvaTS3RLEJtCqWCbnVhrcSFBkDLSV6KMpP6as4mAhLI 8/SzN3vhdsaxrY4DUlIUVv5l4Snf8sPdiuyOVTJCm6AL/KDJDTOwof6bb72GtgyxK1E8ga9v zqWCRqpJjOYizzgTAyiK8lFliSaJwBTsY37eR12T23iRdfnLBC3LZUk6F9+ia1xjXTMO2kGN DF6eE4Ytbyc4xRThfBnEnBA5H5oRQFhsy2CqezZI5MX9/ZnH3Ys/wq7yH0gzrpO8CxNSLp+k zCUq99nplDgn+WSmGIPuPVmoS0NgYOCuEQkNKnEpMAoZA== IronPort-Data: A9a23:ecG/EqPyOHtZMY/vrR3Xk8FynXyQoLVcMsEvi/4bfWQNrUol1zYOy mMYXWiBaKyMNmH1ed8iPo3g9xkOuMWBnYJlGnM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48D8hk/jOHuehYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f7nWQtWo4ow/jb8k035a6q4GlwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gvx4xc3B9q5pa3we0sMT6S6FVDmZq1+BsBOKjAbzsAD+v5T2Mg0MS+7uB3V9zxF8 +ihgLTrIesf0gIgr8xGO/VQO3kW0aSrY9YrK1Dn2SCY5xWun3cBX5yCpaz5VGEV0r8fPI1Ay RAXACkyMyCZg86K+YnhT7Rr1+IBLs7CDqpK7xmMzRmBZRonaZnZRqTR+dJR0HE7jdsIGPfXY stfZDZyBPjCS0QeYBFMUdRuzaH27pX8W2UwRFa9qqcw7Wb7xxc31bnkNduTd9CXLSlQth/D+ D+bozihWnn2MvSl1GW761O+rNaWuh3/Zb8WOe3mzsFD1Qj7Kms7VERMCwflyRWjsWa1Utdbb kgV4TYGtrk37EXtT9/nXhT+rmTsg/IHc9NKFuwh9AyExuzf+ECcB2EBT3hMZMFOWNIKqSICz 2DUr8ntKQBWi+eQFHXM0JWWqhqAEH1ARYMdXhPoWzfp9DUKnW3ephvVS9d4DKO8gpv+Anf1w jmPrW4zi6h7YS83O0eToQqvb9GE/MShousJCuL/BDLN0++BTNT5D7FEEHCChRuARa7AJrV7g JT7pyRuxLxXV8/RykRhsc0QGrC36uyeMSHNyVlhV5wg/jGsk0OekEE5yG8WGXqFxe5dIWa1O BaJ510OjHKRVVPzBZJKj0uKI5xC5cDd+R7ND5g4t/IfM8QjRxzN5yx0e0+b0kbklUVmw+l1O o6WfYzoRTwWALhuhmj+DeoM864Z9gZnz0PqRLf/00uG15iabyWrUrsrCgaFQd04y6Kmmz/r1 ehjGfGE8DhhddHvQzL29NcTJG8aLHJgCpHRrddWR9G5IQFnOT8ADtHAy4wlaYBKoaRnvbrKz yqYR0VnzFr1un7aGzqwM1Fid7LdcpJtpl0rPSEXHAiJ2lpyRa2N/asgZ58MUr1/z9NazNlwV KMjaeibJ/Z+VQT85DUWaKfioLxYdBiEgRyEOwynamMde6FMahPo+Ni+WCfS7wgLUzSKsPUhr 42a1g/0RYQJQyJgBp30bNOt11aAgmgPqtltXkfnIshhR2u0ydJEcxfOt/4QJ90ADT7hxTHAj gafPko+lNn3+oQw9IHEuLCAo4KXCNBBJ0t9HVTAzLOIJCLfr3uCw4hBbb6yRgrjdljIoYesW eYE6MvHEqwjvE1LuI9CAbpU3foAx9/wlYR7kCVgPlv2NmqONJ0xDEWC78d1so91+oR4oiqzA 0KGxclbM+6GOeTjC18gGzAmZeWii9ARvCv26K0tEXqj/AtywrmLamRJHhy2kCcGBqBEAIAk5 uYAucAt9A20jCQxAOuGlix582etLGQKdacsprU2IdXOpFIw61dgZZf8NHfH0KuXYY8RDnhwc y6muqXSop99mGzASiMXPlrQ17N/gZ8uhkh7/GUaLQ7Upuuf1+4F5zwPwzEZVQ8P8w5m1dh0M W1VN0FYA6WC0jNrpcpbVVCXBABzK0yFy3P11mc2ujXVf2uwWkzJCV8NC+KH0UQa0mBbJxxw3 rWTzkT7WjfLIuD1+AYPWnBelv+yduwpqzX+m/2mEf+VQLg8Qz7u2ZG1aUQy9hDIPMIWhW/8n 9dMwtpeU6PAGBQrk/UJMLXCjbU0YzKYFVNGWsBkrf8oH3mDWTSc2gquCkGWe+FPLO2X7UaHJ dBnHZ9LZTSD1QKljDMSNYgTKZBawd8r49sjfOvwBGgk6rGwkBtggKjyxAPf2lA5co5LqtksD IH7exapMH2itVENl0Dj9MB7a3eFO/8abwjC7cWJ2eQuFaNbltpzcEs3g4CGj1/MPCRJpxur7 R7+PYnIxOlfyKNprYvmMoNHIy6WcdrTduC5wDqfguR0T+HkEJnx7lsOi1zdIQ5pE6MbWI13m ZSzodfH5h75k4hsYV/JuauqNvdv3tqzbtp1I8isDXh9nAm+YuHOzSYH2ViFLc1urIsAyOihH ge2UZ7lP5pdEdJQ32ZcZCViAg4QQfa/JLvpoSSm6e+AEF4B2AjAN8mq7mLtcXodTCITJpniE UXhjp5CPDyDQFhkX3foxs2KAqOU5HfqQ64nbMH8vDXeBWKzxFaDs77j0xcs9Fknz5VC/NnSu fr4qtrWLXxee50kCPlSqMp3vxQSDTBwjfRYkoc15Yttkz7jZIIZBb11DHjFY624VgT5z9f9Z TjIbS0vBTiVsfGot/njyIyLYzpzzdDi9js0yvLFMq9Uh+qL6Fu8PYZc IronPort-HdrOrdr: A9a23:zM6vHqhcJEQ4U9ouUsuQQ+kZI3BQXrAji2hC6mlwRA09TyX2ra +TdZggtCMc9gx+ZJhIo7npU5VoKkm3yXca2+Qs1PuZMDXbhA== X-Talos-CUID: 9a23:fDE59GEfV50CgmWmqmJ+yxMkAMQJTkTmlnKNJB6eK2RuYY+8HAo= X-Talos-MUID: =?us-ascii?q?9a23=3AqP9xbQzURhPe9D0FiuzeiNrAB+CaqJ6zV34UsIc?= =?us-ascii?q?sgpCjCyhNBjOw3GqPfaZyfw=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="6.21,241,1763420400"; d="scan'208";a="136554400" X-MGA-submission: =?us-ascii?q?MDFmEg5JyV0+lqxzF6q1ZPhogeKVMhdc3hm58I?= =?us-ascii?q?8PLA8l0vjGdD4Zx2LRth6vb8wo2cQiCM039P30rLjzbrZ2yW0Xq9uaSR?= =?us-ascii?q?R/k5O43RsfB7xVgfs4uhce8upqW9PshxFTwFDuPhiIYY4jZ4ctG9sThH?= =?us-ascii?q?m2zHEAMJB3VE+r9Nn3bgF38Q=3D=3D?= Received: from armistead.cs.miami.edu (HELO armistead.ccs.miami.edu) ([192.31.89.6]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 20 Jan 2026 21:02:42 +0100 Received: by armistead.ccs.miami.edu (Postfix, from userid 3640) id A7CCEA0190F; Tue, 20 Jan 2026 15:02:28 -0500 (EST) To: User-Agent: mail (GNU Mailutils 3.14) Date: Tue, 20 Jan 2026 15:02:28 -0500 Message-Id: <20260120200228.A7CCEA0190F@armistead.ccs.miami.edu> From: geoff@cs.miami.edu X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] Vampire 2026 workshop at FLoC 2026 Reply-To: geoff@cs.miami.edu X-Loop: caml-list@inria.fr X-Sequence: 19433 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: , List-Subscribe: , List-Unsubscribe: , List-Post: List-Owner: List-Archive: Archived-At: The Vampire 2026 workshop will discuss recent developments in implementation, application, evaluation and comparison of first-order theorem provers, including but not limited to Vampire, and their interaction with other systems. We seek submissions reporting on but not limited to: - prerequisites for substantial progress in theorem proving tools - implementation principles and practice - heuristics and strategies for different application areas - case studies, successful and unsuccessful - missing features in modern theorem provers Submissions can be in any form, ranging from work in progress to completed work. For example, the users can submit: - extended abstracts or full papers; - theoretical papers; - experimental papers and case studies; - or in general any papers that can benefit tool developers and users. Papers can be of any length, ranging from 1-page abstracts to full papers up to 20 pages in length. The papers should use the EasyChair templates, which can be found at https://easychair.org/publications/for_authors Submissions should be made using the FLoC system, via the link https://submissions.floc26.org/vampire/ The workshop post-proceedings will be published within the EasyChair EPiC Series in Computing. Important dates: Paper submission: May 29, 2026 (AoE) Notification of acceptance: June 5, 2026 Workshop: July 24, 2026