coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andrei Popescu <andrei.h.popescu AT gmail.com>
- To: coq-club AT inria.fr, dl AT dl.kr.org, folli AT folli.info, fom AT cs.nyu.edu
- Subject: [Coq-Club] PhD or Postdoc Position at LMU Munich about Verified Modal Logics
- Date: Fri, 10 Mar 2023 00:10:06 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andrei.h.popescu AT gmail.com; spf=Pass smtp.mailfrom=andrei.h.popescu AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f171.google.com
- Ironport-data: A9a23:yBs7vK+Zj1CTbLWL1GgLDrUDX3qTJUtcMsCJ2f8bNWPcYEJGY0x3m 2pLXWjQa//fNzDweIslO962800B75CEzodgT1Y+rH9EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPylYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f4nW8kWo4ow/jb8kg356yj4G9wUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE7MRLKGUxL40k/ONdI15T2 swRBRsER0XW7w626OrTpuhEg80iKIz6I9patCg/lHfWCvEpRZ2FSKLPjTNa9G1o14YeQLCHP ZpfMGU2BPjDS0Un1lM/AZQyhuqpwHm5azpApUmeuII45mHSyEp6172F3N/9Jo3VGZ8OxxzwS mTu51T4PjwbGtKj9nms4yODjd3osDveV9dHfFG/3qcy3Af7KnYoIBYRTB6wpeSzolWvXspWb U0S4Csn66YonHFHVfH4Vhy85W+b51sSAoUJVeI97w6Jx+zf5APx6nU4oiBpR+0DkOsxVzwW0 Fqjvez0KgxmnZacYCfInluLlg+aNS8QJG4EQCYLSwoZ/tXuyL3faDqfHr6P94bl3rXI9SHML yOi93dh2u1C5SIf/+DqogCd2mPESo3hF1Ztvm3qsnSZAhSVjbNJiqSt4FnfqOdfdcOXFwbY+ ncDnMea4aYFCpTleM2xrAclTOHBCxWtamW0bbtT838JqW/FF5mLI9s43d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPa/RY+1CK6OM4oTOvCdkTNrGgk+NSZ8OEi9wCARfV0XZ P93jO72XCpCWPg5pNZIb7tHgeVDKt8CKZP7HMinlXxLIJKRY3maTbptDbd9RrFR0U9wmy2Mq 4w3H5LSlX13CbSiCgGKr9N7BQ1VdRATW8qqw+QJLbXrClQ9SAkc5wr5m+xJl3pNxPQLyI8lP xiVBidl9bYIrSSadFvbMSA7NO+HsFQWhStTABHA9G2AgxALCbtDJo9FH3fuVeh9qr5Q3rRvQ uMbes6NJP1KR36Vs34edJTx5sgqPhiimQvEbWLvbSkdbqxQYVXD2ublWQ/zqwgILC687vUlr 5Oaiwj0fJskRiZZNvjwVs6B9V2LgCUiqLpAZHeQeth3U2fwwbduMB3036MWIdlTCBDtxQm69 gexADUer9bju4UerdvD3/iFi6yLEOJOOFVQMEeGzLSxNAjcpnGCx60ZWsm2XDntbkHG04T8W vd0ltbXL+8isGtRlbZFA5JH7P4b9sT+gb131SFmFyj7VEuqAbZePXW258lDmalTzLt/uwHte Eaw1vRFGLeOKuX3OUUwIVc7U+G9yv0koDnewvArKkHc5iUs3r6mU11XDiacmh5mM7p5H4M08 9gP4PdMxVSEtSMrFdKaggR/1WeGdCUAWpp6kKAqOtbgjw5zx2xSZZDZNDTN36iOTNdyY20KO T6fgZTQi4tMnnTid2UBLlmT/O5/q6lXhjV04g4jHXqrlODBpMcL5zxK0DFuTg1q3hRNiO1yH W5wNnxKH6aF/hY2pc1PQ1GTHxplATuH8HfQ0HoMrnXSFGOzZ1zOLUo8GOeDx18Y+GRiZQpm/ KmU5WLmcDTyduTz43cWdWt6jcf8FPpd2xbnms+1O+ikRbwBfivDkKuiQUEquinXK5o9q2Ofr NY74dsqT7PwMBAhhpESCq6Y8O81Yw+FLmkTesNR1voFMk+EcQ7jxAXUDV66f/5MAPn48UWYL chKDeAXXjSc0Be+lBwqNZQuEZRVwsFwvMEjf4n1L1Eoq7Gc9zplkKzB/xjE2VMEfY9crtYfG KjwKRSySnedlFlFqV/r9cNkAFe1UfMARQ/73d22ztk3KoI+gLlsX30fgrqQlFeJATRj5COR7 V/iZbeJ7ulMyrZMvorLE4dfNjqwMvfDUL+ty1m2luhFfffKPdnE7Q8OmGK6PQ4MZbo1cPZ0n ISrr9TY8h7kvrE3cmaBgLiHNfBDyvuTVdptEPDcDSdljwrbf+G0+DoF2WSzCaIRoeNn/sP9G jeJMpqhR+AaS/J25SNzaREHNz0/Fq6uTKPrhR3lnsS2EhJHjDD2doK2x0TIM1NeWDQDYaDlK wnOvP2r2NBUgaJMCDIABNBkG5VIG0Dia4R3a+zOsSSkMUfwjmOgorfCkT8S2QPPAFSAE+f45 svLeEGvPlD68qTF18pQvIFOrwUaRiQ1y/U5ekUGvcV6kXamBWoBNv4QKogCFooSqCHpyZXkf 3vYWQPO08kmsehsKn0QIegPXztzwsQLM9b9Yy02pgaaMnjvQoyHB7Rl+2Fr5HIelv4PCg24A Yl2x5EyFkHZLlJVqSI76fmygOMhzfTfrp7N0V6oiNT8Wn7yHp1TvEGM32NxuejvHMTElUGNL m8wLYyBrIdXVmapeftdl7Vp9N31cd8hI/jErctC/ToHh7im8Q==
- Ironport-hdrordr: A9a23:a45KtKNhwbKHAcBcTsKjsMiBIKoaSvp037BN7TEWdfU1SL3+qy nKpp4mPHDP+VUssR0b+exoW5PgfZq/z+8W3WB5B97LNzUO01HYSb2Kg7GSpwEI2BeTygee78 pdmmRFZ+EYxGIVsfrH
- Ironport-phdr: A9a23:SMgraxTFPeTCcBeAgmjonIfkHNpsogiVAWYlg6HPa5pwe6iut67vI FbYra00ygOTAMOBsq0P0rWempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wE ZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmjqwbalsI BmrrwjdudQajIl/Iast1xXFpWdFdOtRyW50P1yYggzy5t23/J5t8iRQv+wu+stdWqjkfKo2U KJVAi0+P286+MPkux/DTRCS5nQHSWUZjgBIAwne4x7kWJr6rzb3ufB82CmeOs32UKw0VDG/5 KplVBPklCEKPCM//WrKiMJ/kbhbrQquqBJ/zYDaY5ybOuRica3SZt4aWXNBU9xNWyBdHo+xb Y0CBPcBM+ZCqIn9okMDoAe4BQaxHuPg1D5IjWLs0609y+QuDxrG0xA9H9kTt3nbttP1O7oIU e+rzanE1zXDY+lO2Tf68IjHbAshru2RXb9rfsrRzFMgFwLBjlmKtYPlODaV2/0LvmOG4OVuS fihhHQ7qwFtvDev3MEsh5HJiIwa113K9SZ0zok6K9O4SEB2Y9ypHZlQui2ENYZ4Td4vTm5qt Sg0xLMItoC3cTYKxZonyRDSa/+KfoeV7x79UuuaPDR2hGp9db6hmxq/9VKsx+78W8WuzVpGs ClInsPRun0PyhDe7NWMROFn8Ue7wzmP0hje6uFaLkAwkqrWM5shzaQxlpoXqEjCHiH3lFjvg K+Ya0kp+PWk5/7oYrXhoZ+cOIt0hR/kPqsyncy/BPw0MgkIX2eF5eSxzKPv8VH9TblQjfA7k rPVvI3EKckYvKK1Hg1Y3ps75xa6FTim0dAYnXcdLFJCfRKKl5LmO1fTL/DiE/i/gk6gkDdxy /DeOb3hGovCLmPfn7f8Zrt95EtcxxAyzdBb/Z5bFrYBIPfrVk/3r9PXFgU5PBCsw+b7FNV90 ZsTVX+XDq+DLKzSqUOI5v4oI+SUeIAVvy/9J+E56P7qkH82gkQQfbKp3JsScHC3BO5qI0SfY Xr2g9cOC30GvgQkTL+itFrXWjlKIn22QqgU5zchCYvgA52HDoypqLCFmiShWJpMaSQOBFeIF XbAeYKAX/ZKaSScJYspnDsBfbO6DYkwyFejuBKp5aBgK7/9/CECuJOr7N9t6vbYiFlm/Dp4F cmclWHLV2Zsk3gDWhc52al+pQp2zVLVgvswuOBRCdEGv6ABaQw9L5OJl4SSavj3UwPFJZKST Uq+B86hGXc3R84wxNkHZwB8Hc+jh1bNxXniGKcbwpqMApF86afAxz7pPc8ownDKzqQgyVlgW sxXOHatm4Zw8gHSA8jClEDK372ye/Ek1TXWvHyG0XLIuUhZVABqVqCQVHYTfEbX69S//kTaQ qSlFJwoNwJAzYiJLa4ZIsbxgwBgQ/HucM/bf3r3m2q0AkOQwaiQaYPxZ2gH9CDUCUxBgh9Ku HjfalF4CSCmrGbTSjdpEDoDemvK9u9z4DO+R04wlESRalF5kqGy4lgTjOCdTPUa2vQFvj0go nN6BgT12dWeENeGqwd7GccUKdog/FdK037YvA1hL9ShKa5lnFsXbwVwuQvnyRx2DoxKlcVio mktyUJ+LqeR0VUJcD39v9i4M7vbMGTzuhDpc6nO10rVzf6Z/64O7LIzrFCi9AClG0w+8ml2h sFP2ij5hN2CBw4TXJTtF0cvokIi9veKP29kvdOSjCI1YszW+nfY1tkkBfUo0EOldtZba+afE RPqVtYdH46oIfArnF6galQFOvpT/eg6JZDDFbPO1ai1MeJnhD/jg35A5dU320SA7Sd9DO6Ox 5EdzuqTwyOIUj79iBGqtcW9yuUmLXkCW3GyzyTpHtsbb6t+Z4sKT2foO8qvy851mrbiXndZ8 BioAFZMi6rLMVKCKlf62wNXz0Eep3eqzDC5wzJDmDYstqOD3SbKzowObTI/M3VQDClnhFboe s2viswCGVOvd04vnQek4kDzw+5aor5+Ji/dWxUAcy/zJmBkGqy+09jKK8dJ5IklsGNXFvy7e V2BQaPVrB4T0ielFGxbjDw2bDClvJzlkgcy0jrMaiYu6iODKYcpmk6X7ce5J7YZxjccQShkl TTbTkOxOdWk55TclpvOtPy/S3P0U5RSdSfxyobT0UnzrWZuABC5g7Wygoi9SVl8gXK9joM6E 3yX9UWZAMGjzamxPON5c1M9AVb975E/AYRiis4rg4lW33EGh5KT9H5BkGHpMNwd17itCRhFD TMN3dPR5xDonUN5KXfcjYv/Wm+Qw41hIcG9em4N0T8V4MVDCaPS57tB13gQwBLwvUfKbP5xk y1Ig/Io5GQXgqcJ/hIq1iiGCa06EkxRPCiqnBONpYPbzu0fdCOkdr6+01B7lNaqAeSZow1Sb 33+f48rAS566sgseEKJynD47ZvoPcXBdd9G/APBiA/O1qIGTfB53upPnydsPnjx+GEo2/Jux wI7xom05cCGMzk/p///W08AcGepOIVLvWuxxadGwpTIg8b1Rc4nQ2tTGsOvFKPNcnpatOy7Z VjQVmRk8DHDX+KYR1fX6V86/SyRVcr3ZjfHfD9Bio86DBiFeB4A2kZNAHNjz8R/TkfzlKmDO A94/mxDuQK+80ERjLoub16mDC/evFv6M29kDsHAc1wGqFkFvR6dMNTCvLssRGcBr8Hn9ErVb TXFAmYARWARBh7eXwGlbuTovIOQtbDfX7X2LuOSM+/X96oDB7HRlMjpisw/rn6NLpndZCA8S adgiwwYBzYhXJ2I/ldHAzoekyaHByKCjDG7/CA/7sW28fCwHRnq+ZPKELxKd9Nm5xGxh66Hc e+WnidwbzhChNsKwjfTxb4T0UR36WkmfiSxEbkGqS/GTb7B0q5RARkBbipvNcxOp6si1whJM MTfh5v7zLl9xvIyDl5EUxTmlKTLLYQSJHqhMVrcGEuRHLGPJDmO0t6uJK3lFuQWg+JTuBm9/ z2cFg6rPziOkSXoSwH6MexIi3L+XlQWs4W8fxBxTGn7GYi+O1vrbZku121wmOJt1RaofSYGP DNxcl1AtOiV5CJc2bBkHnBZq2FiNa+CkjqY6O/RLtAXt+FqC2J6jbE/gjxyxr1L4SVDXPEwl jHVq4skqleqiOSOjDohSB1Wpy1AmaqEuExjPePS8ZwKChOmtFodqH6dDRgHvY4vEtr0p6VZ0 cTCjor2ITZGtsPLpI4SXpeNbs2AN3UlPFziHzueX25nBXa7cGrYgUJaivSb8HaY+4M7ppbbk 50LUrZHVVYxG5vy5WxqGdUDJNF8WTZ2yNZzaeYH4HO/qF/aQ8AI5vgvt9qXCPTrbSeG1PxKP kRRh7z/KosXO8vw3EkwMjFH
- Ironport-sdr: 640a756b_x7ZG9vwQMtCYI6hHBRsNGGAo+azfhIPddc4paw58d1A9Juu 4JPF3uWG87oeByQ9TrTbpjkU0mENRVmlnFJ/w0g==
We are looking for a PhD student (4 years) or postdoctoral researcher
(3 years) to work on the Isabelle formalization of modal model theory.
The work will take place within the Chair of Theoretical Computer
Science at LMU Munich under Jasmin Blanchette's supervision with the
participation of two external experts: Cláudia Nalon (University of
Brasília) and Sophie Tourret (Inria Nancy).
Modal logics are extensions of classical logics with operators that
allow for the qualification of truth. Model theory for modal logics is
concerned with the interplay between the language (syntax, i.e., the
set of its formulas) and its meaning (semantics, i.e., the structures
over which the language is interpreted). There are, however, different
ways of characterizing meaning for modal sentences and also several
(well-established) results that allow for restriction on the sets of
structures being considered. This project concerns the formalization
in Isabelle of those results for general Kripke structures for
generalized modal operators (i.e., of any arity). The goal is to
produce a library that could then be used (and possibly extended) for
specific applications, in particular those related to proof theory.
The position is categorized as TV-L E13 according to the German salary
scale. It includes some teaching obligations. The starting date is
flexible. Please contact Jasmin Blanchette
(jasmin.blanchette AT ifi.lmu.de) for more information or if you want to
apply. The application deadline is 15 April 2023.
- [Coq-Club] PhD or Postdoc Position at LMU Munich about Verified Modal Logics, Andrei Popescu, 03/10/2023
Archive powered by MHonArc 2.6.19+.