A key component of security in decentralized blockchains is proof of opportunity cost among block producers. In the case of proof-of-work (PoW), currently used by the most prominent systems, the cost is due to spent computation. In this paper, we characterize the security investment of miners in terms of its cost in fiat money. This enables comparison of security allocations across PoW blockchains that generally use different PoW algorithms and reward miners in different cryptocurrency units. We prove that there exists a unique allocation equilibrium, depending on market prices only, that is achieved by both strategic miners (who contemplate the actions of others) and by miners seeking only short-term profit. In fact, the latter will unknowingly compensate for any attempt to deliberately shift security allocation away from equilibrium. Our conclusions are supported analytically through the development of a Markov decision process, game theoretical analysis, and derivation of no arbitrage conditions. We corroborate those results with empirical evidence from more than two years of blockchain and price data. Overall agreement is strong. We show that between January 1, 2018 and August 1, 2020, market prices predicted security allocation between Bitcoin and Bitcoin Cash with error less than 0.6%. And from the beginning of October 2019, until August 1, 2020, market prices predicted security allocation between Bitcoin and Litecoin with error of 0.45%. These results are further corroborated by our establishment of Granger-causality between change in market prices and change in security allocation. To demonstrate the practicality of our results, we describe a trustless oracle that leverages the equilibrium to estimate the price ratios of PoW cryptocurrencies from on-chain information only.

We describe a Martin-Lof style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) computations. We mediate between HOAS representations and computations using contextual modal types. Our type theory also supports an infinite hierarchy of universes and hence supports type-level computation -- thereby providing metaprogramming and (small-scale) reflection. Our main contribution is the development of a Kripke-style model for Cocon that allows us to prove normalization. From the normalization proof, we derive subject reduction and consistency. Our work lays the foundation to incorporate the methodology of logical frameworks into systems such as Agda and bridges the longstanding gap between these two worlds.

All public blockchains are secured by a proof of opportunity cost among block producers. For example, the security offered by proof-of-work (PoW) systems, like Bitcoin, is due to spent computation; it is work precisely because it cannot be performed for free. In general, more resources provably lost in producing blocks yields more security for the blockchain. When two blockchains share the same mechanism for providing opportunity cost, as is the case when they share the same PoW algorithm, the two chains compete for resources from block producers. Indeed, if there exists a liquid market between resource types, then theoretically all blockchains will compete for resources. In this paper, we show that there exists a resource allocation equilibrium between any two blockchains, which is essentially driven by the fiat value of reward that each chain offers in return for providing security. We go on to prove that this equilibrium is singular and always achieved provided that block producers behave in a greedy, but cautious fashion. The opposite is true when they are overly greedy: resource allocation oscillates in extremes between the two chains. We show that these results hold both in practice and in a block generation simulation. Finally, we demonstrate several applications of this theory including a trustless price-ratio oracle, increased security for blockchains whose coins have lower fiat value, and a quantification of cost to allocating resources away from the equilibrium.

We describe a Martin-Lof-style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) computations. We mediate between HOAS representations and computations using contextual modal types. Our type theory also supports an infinite hierarchy of universes and hence supports type-level computation thereby providing metaprogramming and (small-scale) reflection. Our main contribution is the development of a Kripke-style model for Cocon that allows us to prove normalization. From the normalization proof, we derive subject reduction and consistency. Our work lays the foundation to incorporate the methodology of logical frameworks into systems such as Agda and bridges the longstanding gap between these two worlds.

Bisimulation proofs play a central role in programming languages in establishing rich properties such as contextual equivalence. They are also challenging to mechanize, since they require a combination of inductive and coinductive reasoning on open terms. In this paper, we describe mechanizing the property that similarity in the call-by-name lambda calculus is a pre-congruence using Howe's method in the Beluga formal reasoning system. The development relies on three key ingredients: (1) we give a higher order abstract syntax (HOAS) encoding of lambda terms together with their operational semantics as intrinsically typed terms, thereby avoiding not only the need to deal with binders, renaming and substitutions, but keeping all typing invariants implicit; (2) we take advantage of Beluga's support for representing open terms using built-in contexts and simultaneous substitutions: this allows us to directly state central definitions such as open simulation without resorting to the usual inductive closure operation and to encode very elegantly notoriously painful proofs such as the substitutivity of the Howe relation; (3) we exploit the possibility of reasoning by coinduction in Beluga's reasoning logic. The end result is succinct and elegant, thanks to the high-level abstractions and primitives Beluga provides. We believe that this mechanization is a significant example that illustrates Beluga's strength at mechanizing challenging (co)inductive proofs using HOAS encodings.

Abrupt changes in the miner hash rate applied to a proof-of-work (PoW) blockchain can adversely affect user experience and security. Because different PoW blockchains often share hashing algorithms, miners face a complex choice in deciding how to allocate their hash power among chains. We present an economic model that leverages Modern Portfolio Theory to predict a miner's allocation over time using price data and inferred risk tolerance. The model matches actual allocations with mean absolute error within 20% for four out of the top five miners active on both Bitcoin (BTC) and Bitcoin Cash (BCH) blockchains. A model of aggregate allocation across those four miners shows excellent agreement in magnitude with the actual aggregate as well a correlation coefficient of 0.649. The accuracy of the aggregate allocation model is also sufficient to explain major historical changes in inter-block time (IBT) for BCH. Because estimates of miner risk are not time-dependent and our model is otherwise price-driven, we are able to use it to anticipate the effect of a major price shock on hash allocation and IBT in the BCH blockchain. Using a Monte Carlo simulation, we show that, despite mitigation by the new difficulty adjustment algorithm, a price drop of 50% could increase the IBT by 50% for at least a day, with a peak delay of 100%.

We present Tores, a core language for encoding metatheoretic proofs. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types and a form of recursion over objects in the index language to build new types. The latter, which we call index-stratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination.

We present Tores, a core language for encoding metatheoretic proofs. The novel features we introduce are well-founded Mendler-style (co)recursion over indexed data types and a form of recursion over objects in the index language to build new types. The latter, which we call indexstratified types, are analogue to the concept of large elimination in dependently typed languages. These features combined allow us to encode sophisticated case studies such as normalization for lambda calculi and normalization by evaluation. We prove the soundness of Tores as a programming and proof language via the key theorems of subject reduction and termination. 2012 ACM Subject Classification Theory of computation → Type theory, Theory of computation → Logic and verification

Indexed data types allow us to specify and verify many interesting invariants about finite data in a general purpose programming language. In this paper we investigate the dual idea: indexed codata types, which allow us to describe data-dependencies about infinite data structures. Unlike finite data which is defined by constructors, we define infinite data by observations. Dual to pattern matching on indexed data which may refine the type indices, we define copattern matching on indexed codata where type indices guard observations we can make. Our key technical contributions are three-fold: first, we extend Levy's call-by-push value language with support for indexed (co)data and deep (co)pattern matching; second, we provide a clean foundation for dependent (co)pattern matching using equality constraints; third, we describe a small-step semantics using a continuation-based abstract machine, define coverage for indexed (co)patterns, and prove type safety. This is an important step towards building a foundation where (co)data type definitions and dependent types can coexist.

Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple non-nested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e. the multi-step reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong and weak normalisation: a term of the original language is strongly/weakly normalising in one language if and only if it is so in the other. In the proof we develop more general criteria which guarantee that extensions of abstract reduction systems are conservative and preserve strong or weak normalisation.

Reasoning about finite data such as lists or even lambda terms is well understood and programming languages and proof systems o↵er extensive support to inductively define such finite data. Beyond encoding such structures in a simply typed setting, indexing types allows us to enforce even more precise invariants about inductive objects; for example, we may index lists with their length to reason about their size or index lambda-terms with their types to guarantee that we are only working with well-typed objects and our interpreter is type preserving. The dual notion of induction is coinduction, which enables representing and reasoning about infinite data such as processes or streams. Unlike the latter, current representations of coinduction have been proven to be unsatisfactory, either because their lack of elegance makes them di cult to use and reason about or because they break desirable properties (for example subject reduction is broken in Coq [4][7]). We have proposed in [2] the idea to think of infinite data as defined by observations and characterize the result of each observation using copatterns. We then demonstrated in [1] how to guarantee that programs in this language are productive. In this line of work, infinite structures are defined by observations, and finite data, defined by constructors, can be mixed. In this talk, we investigate how to extend the idea of defining infinite data by allowing observations to be indexed by a domain. This is dual to indexing constructors with a domain. Just as in the inductive case, this indexing gives us the ability to reason about infinite structures and fix specifics invariants, together with the possibility to define coinductive predicates or relations. Our extension towards indexed types is restricted to Beluga’s type system. Beluga [3][8][9] is a twolevels language. The first one is an implementation of the logical framework LF [5]. The other level is a functional programming language environment supporting dependent types and pattern matching on LF data. We have developed an extension to Beluga that permits defining indexed observations and writing corecursive/recursive programs about them. Since our observations are defined as records, indexing obeservations correspond to indexed records; as far as we know, indexed records have been absent in dependently typed programming. While dependent records allow latter fields to depend on earlier ones, they typically do not allow us to distinguish between fields based on an index. We demonstrate the elegance and power of indexed observations using three examples: 1) Indexing a stream of bits by a natural number indicating how many bits have been read so far. These indices allow us to certify programs reading sequences of bits of fixed length from the stream and modifying them. 2) The divergence of evaluation of lambda terms with evaluation inside lambda abstractions. In particular, we will prove that ( x.x x) ( x.x x) diverges. 3) A type-preserving environment-based interpreter where we represent closures coinductively following ideas by Milner and Tofte [6]. Our prototype is the first programming environment that supports coinductive reasoning about LF specifications. This will allow us to explore new applications such as bisimulation proofs and proofs about contextual equivalence. We are currently extending and adapting our prior work on copatterns [2] to indexed copatterns in Beluga. More broadly, we see our work which restricts dependencies to a decidable domain as an interesting step towards supporting copatterns in a fully dependently typed languages.

Inductive datatypes provide mechanisms to define finite data such as finite lists and trees via constructors and allow programmers to analyze and manipulate finite data via pattern matching. In this paper, we develop a dual approach for working with infinite data structures such as streams. Infinite data inhabits coinductive datatypes which denote greatest fixpoints. Unlike finite data which is defined by constructors we define infinite data by observations. Dual to pattern matching, a tool for analyzing finite data, we develop the concept of copattern matching, which allows us to synthesize infinite data. This leads to a symmetric language design where pattern matching on finite and infinite data can be mixed. We present a core language for programming with infinite structures by observations together with its operational semantics based on (co)pattern matching and describe coverage of copatterns. Our language naturally supports both call-by-name and call-by-value interpretations and can be seamlessly integrated into existing languages like Haskell and ML. We prove type soundness for our language and sketch how copatterns open new directions for solving problems in the interaction of coinductive and dependent types.

Termination is an important property for programs and is necessary for formal proofs to make sense. In order to make sure that a program using recursion is terminating, one can use a termination checker that will use some strategy to verify the termination of a given program. Two very common strategies are structural recursion that makes an analysis on the structure of terms and sized types that use size annotation in the types. In this paper, we compare the two approaches to identify their strengths and limitations and to see how one can proceed to prove termination using each of the strategies. This analysis is done on different examples: a series of functions on the natural numbers and a mergesort algorithm. We also discuss the use of each of the approaches in the cases of proofs.

Proof-of-work blockchains must implement a difficulty adjustment algorithm (DAA) in order to maintain a consistent inter-arrival time between blocks. Conventional DAAs are essentially feedback controllers, and as such, they are inherently reactive. This approach leaves them susceptible to manipulation and often causes them to either under- or over-correct. We present Bonded Mining, a proactive DAA that works by collecting hash rate commitments secured by bond from miners. The difficulty is set directly from the commitments and the bond is used to penalize miners who deviate from their commitment. We devise a statistical test that is capable of detecting hash rate deviations by utilizing only on-blockchain data. The test is sensitive enough to detect a variety of deviations from commitments, while almost never misclassifying honest miners. We demonstrate in simulation that, under reasonable assumptions, Bonded Mining is more effective at maintaining a target block time than the Bitcoin Cash DAA, one of the newest and most dynamic DAAs currently deployed. In this preliminary work, the lowest hash rate miner our approach supports is 1% of the total and we directly consider only two types of fundamental attacks. Future work will address these limitations.