اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدMechanizing the Metatheory of LF
108
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
LF is a dependent type theory in which many other formal systems can be conveniently embedded. However, correct use of LF relies on nontrivial metatheoretic developments such as proofs of correctness of decision procedures for LFs judgments. Although detailed informal proofs of these properties have been published, they have not been formally verified in a theorem prover. We have formalized these properties within Isabelle/HOL using the Nominal Datatype Package, closely following a recent article by Harper and Pfenning. In the process, we identified and resolved a gap in one of the proofs and a small number of minor lacunae in others. We also formally derive a version of the type checking algorithm from which Isabelle/HOL can generate executable code. Besides its intrinsic interest, our formalization provides a foundation for studying the adequacy of LF encodings, the correctness of Twelf-style metatheoretic reasoning, and the metatheory of extensions to LF.
قيم البحث
اقرأ أيضاً
We present a system called Adelfa that provides mechanized support for reasoning about specifications developed in the Edinburgh Logical Framework or LF. Underlying Adelfa is a new logic named L_LF. Typing judgements in LF are represented by atomic f
ormulas in L_LF and quantification is permitted over contexts and terms that appear in such formulas. Contexts, which constitute type assignments to uniquely named variables that are modelled using the technical device of nominal constants, are characterized in L_LF by context schemas that describe their inductive structure. We present these formulas and an associated semantics before sketching a proof system for constructing arguments that are sound with respect to the semantics. We then outline the realization of this proof system in Adelfa and illustrate its use through a few example proof developments. We conclude the paper by relating Adelfa to existing systems for reasoning about LF specifications.
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 gluing together diverse Type Theorie
s and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the CMU School. The first system, CLLFP, is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLFP?, features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value lambda-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms.
Location fingerprint (LF) has been widely applied in indoor positioning. However, the existing studies on LF mostly focus on the fingerprint of WiFi below 6 GHz, bluetooth, ultra wideband (UWB), etc. The LF with millimeter-wave (mmWave) was rarely ad
dressed. Since mmWave has the characteristics of narrow beam, fast signal attenuation and wide bandwidth, etc., the positioning error can be reduced. In this paper, an LF positioning method with mmWave is proposed, which is named as DoA-LF. Besides received signal strength indicator (RSSI) of access points (APs), the fingerprint database contains direction of arrival (DoA) information of APs, which is obtained via DoA estimation. Then the impact of the number of APs, the interval of reference points (RPs), the channel model of mmWave and the error of DoA estimation algorithm on positioning error is analyzed with Cramer-Rao lower bound (CRLB). Finally, the proposed DoA-LF algorithm with mmWave is verified through simulations. The simulation results have proved that mmWave can reduce the positioning error due to the fact that mmWave has larger path loss exponent and smaller variance of shadow fading compared with low frequency signals. Besides, accurate DoA estimation can reduce the positioning error.
In this work, to measure the accuracy and efficiency for a latency-controlled streaming automatic speech recognition (ASR) application, we perform comprehensive evaluations on three popular training criteria: LF-MMI, CTC and RNN-T. In transcribing so
cial media videos of 7 languages with training data 3K-14K hours, we conduct large-scale controlled experimentation across each criterion using identical datasets and encoder model architecture. We find that RNN-T has consistent wins in ASR accuracy, while CTC models excel at inference efficiency. Moreover, we selectively examine various modeling strategies for different training criteria, including modeling units, encoder architectures, pre-training, etc. Given such large-scale real-world streaming ASR application, to our best knowledge, we present the first comprehensive benchmark on these three widely used training criteria across a great many languages.
Process calculi may be compared in their expressive power by means of encodings between them. A widely accepted definition of what constitutes a valid encoding for (dis)proving relative expressiveness results between process calculi was proposed by G
orla. Prior to this work, diverse encodability and separation results were generally obtained using distinct, and often incompatible, quality criteria on encodings. Textbook examples of valid encoding are the encodings proposed by Boudol and by Honda & Tokoro of the synchronous choice-free $pi$-calculus into its asynchronous fragment, illustrating that the latter is no less expressive than the former. Here I formally establish that these encodings indeed satisfy Gorlas criteria.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
