Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userMechanizing the Metatheory of LF
110
0
0.0
(
0
)
Added by
James Cheney
Publication date
2010
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
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.
rate research
Read More
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 formulas 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 Theories 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 addressed. 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 social 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 Gorla. 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.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
