Plugging-in proof development environments using Locks in LF

Autor: Furio Honsell, Luigi Liquori, Ivan Scagnetto, Petar Maksimovic
Přispěvatelé: Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Logical Time for Formal Embedded System Design (KAIROS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbian Academy of Sciences and Arts (SASA), European Project: COST Action CA15123 ,COST - European Cooperation in Science and Technology,EUTYPES(2016), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS)
Jazyk: angličtina
Rok vydání: 2018
Předmět:
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES
Technology
Record locking
0102 computer and information sciences
02 engineering and technology
Type (model theory)
Mathematics (miscellaneous)
Computer Science Applications1707 Computer Vision and Pattern Recognition
Mathematical proof
computer.software_genre
01 natural sciences
Oracle
[INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Computation Theory & Mathematics
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS
Computer Science
Theory & Methods
0202 electrical engineering
electronic engineering
information engineering
Set theory
Mathematics
0802 Computation Theory and Mathematics
Science & Technology
Programming language
PI-CALCULUS
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
MSCS
Intuitionistic type theory
FRAMEWORK
Computer Science Applications
Constraint (information theory)
010201 computation theory & mathematics
Computer Science
020201 artificial intelligence & image processing
Affine logic
Algorithm
computer
Zdroj: Mathematical Structures in Computer Science
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (9), pp.1578--1605
Mathematical Structures in Computer Science, 2018, 28 (9), pp.1578--1605
ISSN: 0960-1295
1469-8072
Popis: We present two extensions of theLFconstructive type theory featuring monadiclocks. A lock is a monadic type construct that captures the effect of anexternal call to an oracle. Such calls are the basic tool forplugging-inand 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 thecanonical styledeveloped by the ‘CMU School.’ The first system,CLLF𝒫, is the canonical version of the systemLLF𝒫, 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 ofCLLF𝒫andCLLF𝒫?permit to factor out naturally the complexities arising from enforcing these ‘side conditions,’ which severely obscure standardLFencodings. We discuss Girard's Elementary Affine Logic, Fitch–Prawitz set theory, call-by-value λ-calculi and functions, both total and even partial.
Databáze: OpenAIRE
Externí odkaz: