Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention

Abstarct We formalize in Constructive Type Theory the Lambda Calculus in its classical first-order syntax, employing only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. As a fundamental part of the formalization, we introduce principles of induction and recursion on terms which provide a framework for reproducing the use of the Barendregt Variable Convention as in pen-and-paper proofs within the rigorous formal setting of a proof assistant. The principles in question are all formally derivable from the simple principle of structural induction/recursion on concrete terms. We work out applications to some fundamental meta-theoretical results, such as the Church–Rosser Theorem and Weak Normalization for the Simply Typed Lambda Calculus. The whole development has been machine checked using the system Agda.

Abstraction Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound with respect to an intuitive and simple algebraic semantics. Completeness holds for both intuitionistic and classical abstraction logic, and all abstraction logics in between and beyond.

Abstraction Logic

Abstraction Logic is introduced as a foundation for Practical Types and Practal. It combines the simplicity of first-order logic with direct support for variable binding constants called abstractions. It also allows free variables to depend on parameters, which means that first-order axiom schemata can be encoded as simple axioms. Conceptually abstraction logic is situated between first-order logic and second-order logic. It is sound and complete with respect to an intuitive and simple algebraic semantics.

Pengaruh Kualitas Produk dan Harga terhadap Keputusan Pembelian Alat-Alat Kesehatan pada PT Inti Medicom Retailindo

Researchers conducted research to find out the influence of free variables product quality and price to the variable bound (buying decision) Medical Devices In PT.Inti Medicom Retailindo.Researchers use quantitative data with questionnaires as a means of collecting data used.The method used by researchers is non probability sampling method with purpose sampling technique.With a sample of 100 people have criteria has been made purchases twice or more in PT.Medicom Retailindo core that will be processed using SPSS version 20 program.The results of this study show if there is an influence of significance of the free variable of product quality and price on medical devices in PT.Inti Medicom Retailindo.Based on the results of the t-count test of the three free variables, product quality variables have a value of 6,534 > ttabel > 1,985, the price has a thitung number of > ttabel of 2,032 > 1,985.While looking at the figures based on the results of the F test that the value of Fhitung > Ftabel = 94,722 > 3,089 this means that variable product quality and price simultaneously affect the purchase decision

A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.

PENGARUH PSAK NO. 1 TENTANG PENYAJIAN LAPORAN CASH FLOW DAN CAPITAL EXPENDITURE TERHADAP FIRM VALUE PADA PERUSAHAAN YANG BERGERAK DI BIDANG CONSUMER GOOD YANG TERDAFTAR DI JAKARTA ISLAMIC INDEX PERIODE 2010-2019

Financial statements are prepared and presented to be submitted to those who need them. Of course, in this presentation must be in accordance with the existing provisions that are stipulated in PSAK No. 1 concerning the presentation of financial statements. Firm Value has an important role because it will form an image for the company, firm value is created by the contribution of other factors. Operation Cash Flow informs cash inflows and cash outflows from a company. Capital Expenditure as a reserve fund to support the expansion of the company or the improvement of assets. This research uses descriptive methods and quantitative approaches using secondary data supported by literature and documentation studies. The results showed that Operation Cash Flow partially has a positive and significant effect on Firm Value as well as Capital Expenditure has a positive and significant effect on Firm Value. Simultaneously both free variables can contribute and are able to significantly affect firm value.Keywords: Operation Cash Flow, Capital Expenditure, Firm Value

Pengaruh Likuiditas, Kebijakan Hutang, Pertumbuhan Perusahaan dan Ukuran Perusahaan Terhadap Nilai Perusahaan dengan Profitabilitas Sebagai Variabel Intervening pada Perusahaan Sub Sektor Farmasi Di Bursa Efek Indonesia Periode 2014 – 2019

This study is to look at the influence of Liquidity, Debt Policy, Company Growth And Company Size on Company Value With Profitability As Intervening Variable In Pharmaceutical Sub-Sector Companies on Indonesia Stock Exchange Period 2014 - 2019. Liquidity variables that are diproxykan with current ratio, debt policy that is diproxykan with debt to equity ratio, growth of the company that is diproxykan with changes in total assets and the size of the company that is diproxykan with normal logarithm (Ln) sales to the value of the company that is mortgaged with price to book value with profitability diproxykan with return on equity as intervening variables. The research sample used is the Pharmaceutical Sub Sector on the Indonesia Stock Exchange during the 6-year observation period, starting from 2014 - 2019 recorded as many as 10 companies, which have a complete financial report and which have a complete research indicator report in the annual financial report during the research period as many as 8 companies. This study used purposive sampling and data analysis techniques using the help of microsoft Excell and SPSS 22.0 software. with Path Analysis. The results showed that; 1) Simultaneously all free variables have no effect on bound variables whereas that partially only the growth variables of the company are diproxykan with changes in total assets that affect the variable profitability. 2) Simultaneously all free variables have a significant effect on bound variables whereas partially only the growth variables of the company are diproxykan with changes in total assets that have no effect on the variable value of the company. 3) Variable profitability diproxykan with return on equity has no effect on the variable value of the company that is diproxykan with price to book value. 4) Variable liquidity, debt policy, company growth and the size of the company to the value of the company with profitability as an intervening variable has a total influence of 11.1838%, the large influence including weak.

EFFECT OF SELF EFFICACY AND ORGANIZATIONAL CITIZENSHIP BEHAVIORS ON EMPLOYEE SATISFACTION

Human resources become a major problem in various activities within a company, especially in the field of organizational. This research aims to test and analyze the employee satisfaction of PT. Sinar Karya Abadi's work which is influenced by the variable of self-efficacy and behavior of the citizenship organization. The population amounted to 500 employees and obtained samples amounting to 85 respondents consisting of employees of PT. Sinar Karya Duta Abadi. Simple random sampling is a sampling technique that uses the utility. Obtained data from the propagate then recollected the questionnaire and used techniques analyzed multiple linear regression and hypotheses tests. Available work satisfaction results gain influence from free variables. That result illustrates the free variables having an influence on the dependent variables. It is hoped that this research can be used as a reference where PT. Sinar Karya Duta Abadi can improve employee satisfaction through self-efficacy and behavior of the nationality organization, if the two traits are owned by each individual, then the organizational productivity increases.

Tracing sharing in an imperative pure calculus

© 2018 Elsevier B.V. We introduce a type and effect system, for an imperative object calculus, which infers sharing possibly introduced by the evaluation of an expression, represented as an equivalence relation among its free variables. This direct representation of sharing effects at the syntactic level allows us to express in a natural way, and to generalize, widely-used notions in literature, notably uniqueness and borrowing. Moreover, the calculus is pure in the sense that reduction is defined on language terms only, since they directly encode store. The advantage of this non-standard execution model with respect to a behaviorally equivalent standard model using a global auxiliary structure is that reachability relations among references are partly encoded by scoping.