The proceedings contain 11 papers. The topics discussed include: on model-theoretic strong normalization for truth-table natural deduction; extending equational monadic reasoning with monad transformers; towards a certified reference monitor of the android 10 permission system; coinductive proof search for polarized logic with applications to full intuitionistic propositional logic; synthetic completeness for a terminating Seligman-style tableau system; and two applications of logic programming to Coq.
26th International Conference on Types for Proofs and Programs, TYPES 2020
Ugo de'Liguoro
First
;Stefano Berardi;
2021-01-01
Abstract
The proceedings contain 11 papers. The topics discussed include: on model-theoretic strong normalization for truth-table natural deduction; extending equational monadic reasoning with monad transformers; towards a certified reference monitor of the android 10 permission system; coinductive proof search for polarized logic with applications to full intuitionistic propositional logic; synthetic completeness for a terminating Seligman-style tableau system; and two applications of logic programming to Coq.
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
LIPIcs-TYPES-2020-0.pdf
Accesso aperto
Tipo di file:
PDF EDITORIALE
Dimensione
469.28 kB
Formato
Adobe PDF
|
469.28 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
