Search

The concept of computable functions (as developed by Godel, Church, Turing, and Kleene in the 1930's) has been extensively studied, leading to the modern subject of recursive function theory. However recent work by category theorists has led to a more conceptual and abstract foundation of computability theory—Turing categories. A Turing category models the notion of partial map as well as recursive computation, using methods of categorical algebra to formalize these concepts. The goal of this work is to provide a formal framework for analyzing this categorical model of computation. We use the Coq Proof Assistant, which implements the Calculus of (co)Inductive Constructions (CIC), and we build on an existing Coq library for general category theory. We focus on both formalizing Turing categories and on building a general framework in the form of a well-structured Coq library that can be further extended. We begin by formalizing definitions, propositions, and proofs pertaining to Turing categories, and then instantiate the more general Turing category formalism with a CIC description of the category which explicitly models the language of partial recursive functions.

User-defined tokens—both fungible ERC-20 and non-fungible ERC-721 tokens—are central to the majority of contracts deployed on Ethereum. User-defined tokens are non-native on Ethereum; i.e., they are not directly supported by the ledger, but require custom code. This makes them unnecessarily inefficient, expensive, and complex.

Agile software development and Formal Methods are traditionally seen as being in conflict. From an Agile perspective, there is pressure to deliver quickly, building vertical prototypes and doing many iterations/sprints, refining the requirements; from a Formal Methods perspective, there is pressure to deliver correctly and any change in requirements often necessitates changes in the formal specification and might even impact all arguments of correctness.

During the last decades an imbalance in the territorial distribution of population in Russia is increasing. That contributes to the emergence of interethnic tensions. The article is devoted to the process of elaboration of the legal provisions that support internal migration. The author’s attention is focused on decrees of the Russian Federation President related to migration issues and the main trends of the development of legislation in this area. The author explains the necessity of legal regulation of authorities’ power in the area of migration at federal legislation level because of the influence of migration restrictions on constitutional rights of citizens. Creation of effective legal mechanisms of regulation internal migration caused by the need to account the geopolitical interests and the economic and social development of the country and possible change of priorities of trade and economic cooperation, as well as the development of import substitution. The main focus lays on the deterrents for internal migration, overcoming of which is possible by using legal means to identify priority measures. Changing the nature of records at the place of stay from permissive to notification is one of the main instruments that require clarification of the procedures and grounds of such accounting. The availability of the social infrastructure and accessible mechanisms for the use of infrastructure is also an important prerequisite for attracting labor resources. The new institution of law - renting living accommodation for social use and its impact on the development the internal migration are considered in this article as one of said prerequisites. The author has generalized factors of ethnic and religious tension and proposed measures to prevent them.