Search

Your search keyword '"Honsell, Furio"' showing total 9 results
Start Over Author "Honsell, Furio" Publisher hal ccsd
9 results on '"Honsell, Furio"'

1. A prototype-based approach to object reclassification

Author

Ciaffaglione, Alberto, Gianantonio, Pietro, Honsell, Furio, Liquori, Luigi, 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), and Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2020

2. A prototype-based approach to object reclassification

Author

Ciaffaglione, Alberto, Gianantonio, Pietro, Honsell, Furio, Liquori, Luigi, 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), and Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

International audience; We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2020

3. A prototype-based approach to object evolution

Author

Ciaffaglione, Alberto, Di Gianantonio, Pietro, Honsell, Furio, Liquori, Luigi, 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 (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), 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), Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France, Université Nice Sophia Antipolis (... - 2019) (UNS), and 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)

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

International audience; We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2020

4. A protoype-based approach to object reclassification

Author

Ciaffaglione, Alberto, Gianantonio, Pietro, Honsell, Furio, Liquori, Luigi, 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), and Inria & Université Cote d'Azur, CNRS, I3S, Sophia Antipolis, France

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2019

5. A protoype-based approach to object reclassification

Author

Ciaffaglione , Alberto, Gianantonio , Pietro, Honsell , Furio, Liquori , Luigi, Dipartimento di Matematica e Informatica - Universita Udine ( DIMI ), Università degli Studi di Udine - University of Udine [Italie], Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems ( LOGNET ), Inria Sophia Antipolis - Méditerranée ( CRISAM ), and Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria )

Subjects
object reclassification, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, static typing, Prototype-based calculi, [ INFO.INFO-CL ] Computer Science [cs]/Computation and Language [cs.CL], [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

We investigate, in the context of functional prototype-based languages , a calculus of objects which might extend themselves upon receiving a message, a possibility referred to by Cardelli as a self-inflicted operation. We present a sound type system for this calculus which guarantees that evaluating a well-typed expression will never yield a message-not-found runtime error. The resulting calculus is an attempt towards the definition of a language combining the safety advantage of static type check with the flexibility normally found in dynamically typed languages.

Published
2018

6. LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads

Author

Honsell, Furio, Liquori, Luigi, Maksimović, Petar, Scagnetto, Ivan, 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 (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), 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), Université Nice Sophia Antipolis (... - 2019) (UNS), and 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)

Subjects
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Computer aided formal verification, Logical frameworks, Type theory, Typed lambda calculus, Theoretical Computer Science, Computer Science (all), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], MESH: LMCS, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS, [MATH.MATH-LO]Mathematics [math]/Logic [math.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [INFO]Computer Science [cs]
Abstract

International audience; We extend the constructive dependent type theory of the Logical Framework LF with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an LF type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, LLFP, is a conservative extension of LF, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. LLFP arises once the monadic nature of the lock type-constructor, L^P_{M,σ}[-], introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, U^P_{M,σ}[-], in place of Moggi’s monadic let_T, thus simplifying the equational theory. The rules for U^P_{M,σ}[-] permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of LLFP by a novel indirect method based on the encoding of LLFP in LF. We discuss encodings in LLFP of call-by-value λ-calculi, Hoare’s Logic, and Fitch-Prawitz Naive Set Theory.

Published
2017

7. Implementing Cantor's Paradise

Author

Honsell, Furio, Lenisa, Marina, Liquori, Luigi, Scagnetto, Ivan, Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria), and European Project: COST Action IC1201,COST - European Cooperation in Science and Technology,BETTY(2012)

Subjects
[INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], coalgebras, hyperuniverses, Fitch-Prawitz set theory, paradoxes, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], logical frameworks, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], [INFO.INFO-SI]Computer Science [cs]/Social and Information Networks [cs.SI]
Abstract

International audience; Set-theoretic paradoxes have made all-inclusive self-referential Foundational Theories almost a taboo. The few daring attempts in the literature to break this taboo avoid paradoxes by restricting the class of formulae allowed in Cantor's naive Comprehension Principle. A different, more intensional approach was taken by Fitch, reformulated by Prawitz, by restricting, instead, the shape of deductions, namely allowing only normal(izable) deductions. The resulting theory is quite powerful, and consistent by design. However, modus ponens and Scotus ex contra-dictione quodlibet principles fail. We discuss Fitch-Prawitz Set Theory (FP) and implement it in a Logical Framework with so-called locked types, thereby providing a "Computer-assisted Cantor's Paradise" : an interactive framework that, unlike the familiar Coq and Agda, is closer to the familiar informal way of doing mathematics by delaying and consolidating the required normality tests. We prove a Fixed Point Theorem, whereby all partial recursive functions are definable in FP. We establish an intriguing connection between an extension of FP and the Theory of Hyperuniverses: the bisimilarity quotient of the coalgebra of closed terms of FP satisfies the Comprehension Principle for Hyperuniverses.

Published
2016

8. LFP – A Logical Framework with External Predicates (Announcement and survey)

Author

Honsell, Furio, Lenisa, Marina, Liquori, Luigi, Maksimovic, Petar, Scagnetto, Ivan, Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Logical Networks: Self-organizing Overlay Networks and Programmable Overlay Computing Systems (LOGNET), Inria Sophia Antipolis - Méditerranée (CRISAM), and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, ACM: F.: Theory of Computation, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs/F.3.1.3: Mechanical verification, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract

Invited Talk: A peer-refereed Festschrift will be published as a special issue of the JLC journal.; International audience; Throughout the history of Mathematics, several different proof cul- tures have co-existed, and still do co-exist. After 25 years of Logical Frameworks, we can say that even as far as proof metalanguages go, a definitive system is utopian and that we are witnessing the continuous development of a diversity of formal proof cultures, see e.g. [10-12, 17, 19, 21, 23, 24, 28]. In this paper, we propose a contribution towards the clarification of some controversial issues that have arisen in the theory and practice of Logical Frameworks, and have possibly motivated such a manifold speciation. Using as a running example the encoding of the critical features of Non-Commutative Linear Logic (NCLL) [26] in the Logical Framework LFP [20], we discuss the notions of adequacy of an encoding, locality of a side-condition, deep and shallow encodings, and how to embed heterogenous justifications or external evidence in LF. This discussion naturally leads to the question of how to express formally the expressive power of a Logical Framework, a minimal requirement being that of encoding itself within itself. We focus on LFP and we discuss its relations to the original LF[17], and briefly to the Conditional LF [21], and the Pattern LF [19] previously introduced by the authors. We conclude the paper by briefly comparing LFP to λΠ-calculus modulo [12], the Linear LF [9], and the Concurrent LF[28].

Published
2013

9. A Framework for Defining Logical Frameworks

Author

Liquori, Luigi, Honsell, Furio, Lenisa, Marina, Algorithms, simulation, combinatorics and optimization for telecommunications (MASCOTTE), 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), Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Dipartimento di Matematica e Informatica - Universita Udine (DIMI), Università degli Studi di Udine - University of Udine [Italie], Research partially supported by the EU Project FP6-IST-510996 TYPES, and by the French CNRS grant ACI Modulogic, INRIA, Université Nice Sophia Antipolis (1965 - 2019) (UNS), and 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)

Subjects
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Dependent-type systems, Edinburgh's Logical Framework, ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory, Curry-Howard, ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.2: Language Classifications, Logics, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic, Patterns, Pattern matching, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Lambda calculus
Abstract

In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The framework GLF features a generalized form of lambda abstraction where beta-reductions fire provided the argument satisfies a logical predicate and may produce an n-ary substitution. The type system keeps track of when reductions have yet to fire. The framework GLF subsumes, by simple instantiation, LF as well as a large class of generalized constrained-based lambda calculi, ranging from well known restricted lambda calculi, such as Plotkin's call-by-value lambda calculus, to lambda calculi with patterns. But it suggests also a wide spectrum of completely new calculi which have intriguing potential as Logical Frameworks. We investigate the metatheoretical properties of the calculus underpinning GLF and illustrate its expressive power. In particular, we focus on two interesting instantiations of GLF. The first is the Pattern Logical Framework (PLF), where applications fire via pattern-matching in the style of Cirstea, Kirchner, and Liquori. The second is the Closed Logical Framework (CLF) which features, besides standard beta-reduction, also a reduction which fires only if the argument is a closed term. For both these instantiations of GLF we discuss standard metaproperties, such as subject reduction, confluence and strong normalization. The GLF framework is particularly suitable, as a metalanguage, for encoding rewriting logics and logical systems, where rules require proof terms to have special syntactic constraints, e.g. logics with rules of proof, in addition to rules of derivations, such as, e.g., modal logics, and call-by-value lambda calculus.

Published
2006

Catalog

Books, media, physical & digital resources
See catalog results