Formalizing Cut Elimination of Coalgebraic Logics in Coq
Identifieur interne : 002C97 ( Istex/Curation ); précédent : 002C96; suivant : 002C98Formalizing Cut Elimination of Coalgebraic Logics in Coq
Auteurs : Hendrik Tews [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In their work on coalgebraic logics, Pattinson and Schröder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics [1]. The present paper reports on a formalization of Pattinson’s and Schröder’s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.
Url:
DOI: 10.1007/978-3-642-40537-2_22
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002D34
Links to Exploration step
ISTEX:BE8BE82245D58E3196C975CE5104BB08FF28E2FDLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Formalizing Cut Elimination of Coalgebraic Logics in Coq</title><author><name sortKey="Tews, Hendrik" sort="Tews, Hendrik" uniqKey="Tews H" first="Hendrik" last="Tews">Hendrik Tews</name><affiliation wicri:level="1"><mods:affiliation>Institute of Systems Architecture, TU Dresden, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>Institute of Systems Architecture, TU Dresden</wicri:regionArea></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:BE8BE82245D58E3196C975CE5104BB08FF28E2FD</idno><date when="2013" year="2013">2013</date><idno type="doi">10.1007/978-3-642-40537-2_22</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-QNQKDKP3-B/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002D34</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D34</idno><idno type="wicri:Area/Istex/Curation">002C97</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Formalizing Cut Elimination of Coalgebraic Logics in Coq</title><author><name sortKey="Tews, Hendrik" sort="Tews, Hendrik" uniqKey="Tews H" first="Hendrik" last="Tews">Hendrik Tews</name><affiliation wicri:level="1"><mods:affiliation>Institute of Systems Architecture, TU Dresden, Germany</mods:affiliation><country xml:lang="fr">Allemagne</country><wicri:regionArea>Institute of Systems Architecture, TU Dresden</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In their work on coalgebraic logics, Pattinson and Schröder prove soundness, completeness and cut elimination in a generic sequent calculus for propositional multi-modal logics [1]. The present paper reports on a formalization of Pattinson’s and Schröder’s work in the proof assistant Coq that provides machine-checked proofs for soundness, completeness and cut elimination of their calculus. The formalization exploits dependent types to obtain a very concise deep embedding for formulas and proofs. The work presented here can be used to verify cut elimination theorems for different modal logics with considerably less effort in the future.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002C97 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 002C97 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:BE8BE82245D58E3196C975CE5104BB08FF28E2FD
|texte= Formalizing Cut Elimination of Coalgebraic Logics in Coq
}}
| This area was generated with Dilib version V0.6.33. |  |