We present two extensions of the LF constructive type theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for plugging-in and gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in the canonical style developed by the ‘CMU School.’ The first system, CLLF, is the canonical version of the system LLF, presented earlier by the authors. The second system, CLLF?, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms of CLLF and CLLF? permit to factor out naturally the complexities arising from enforcing these ‘side conditions,’ which severely obscure standard LF encodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial.
Plugging-in proof development environments using Locks in LF
HONSELL, FURIO;SCAGNETTO, IVAN
2018-01-01
Abstract
We present two extensions of the LF constructive type theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for plugging-in and gluing together, different metalanguages and proof development environments. Oracles can be invoked either to check that a constraint holds or to provide a witness. The systems are presented in the canonical style developed by the ‘CMU School.’ The first system, CLLF, is the canonical version of the system LLF, presented earlier by the authors. The second system, CLLF?, features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. In order to illustrate the advantages of our new frameworks, we show how to encode logical systems featuring rules that deeply constrain the shape of proofs. The locks mechanisms of CLLF and CLLF? permit to factor out naturally the complexities arising from enforcing these ‘side conditions,’ which severely obscure standard LF encodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial.File | Dimensione | Formato | |
---|---|---|---|
MSCS.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Pre-print
Licenza:
Creative commons
Dimensione
551.47 kB
Formato
Adobe PDF
|
551.47 kB | Adobe PDF | Visualizza/Apri |
MSCS2016.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
520.59 kB
Formato
Adobe PDF
|
520.59 kB | Adobe PDF | Visualizza/Apri |
pluggingin_proof_development_environments_using_locks_in_lf.pdf
non disponibili
Descrizione: Articolo principale
Tipologia:
Versione Editoriale (PDF)
Licenza:
Non pubblico
Dimensione
548.57 kB
Formato
Adobe PDF
|
548.57 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.