title: Abrupt millennial-scale changes in intensity of Southern Hemisphere westerly winds during marine isotope stages 2–4

authors: Whittaker, Thomas Edward

subjects: chemistry

abstract: The strength of mid-southern latitude westerly atmospheric circulation plays an important role in global climate. Due to a lack of long, continuous, high-resolution paleoclimate archives from mid-southern latitudes, it remains unclear what factors control changes in its intensity and how past changes affected the climates of landmasses in their path. Here we show growth rate and stable isotope (18O, 13C) profiles from a South Island, New Zealand, stalagmite (HW3) that permit centennial-scale investigation of Southern Hemisphere westerly paleointensity between 73 and 11 ka. Correlation between HW3 growth rate and isotope profiles suggests sensitivity to changes in annual precipitation, a factor controlled by westerly intensity. Low growth rates and relatively enriched isotope ratios define long-term trends in HW3, supporting existing evidence that weaker westerlies predominated during the last glacial period. Abrupt millennial-scale events occur frequently, such that the HW3 record resembles Greenland ice core stable isotope profiles. Furthermore, nearly synchronous timing of nine prominent wet and cool intervals with Heinrich events supports studies showing that increased westerly intensity is closely linked to North Atlantic cooling. As well as Heinrich events, the HW3 profiles also show an Antarctic Cold Reversal–like event during deglaciation, advocating for a bipolar seesaw of global climate at that time.

text: Abrupt millennial-scale changes in intensity of Southern Hemisphere westerly winds during marine isotope stages 2–4 The strength of mid-southern latitude westerly atmospheric circulation plays an important role in global climate. Due to a lack of long, continuous, high-resolution paleoclimate archives from mid-southern latitudes, it remains unclear what factors control changes in its intensity and how past changes affected the climates of landmasses in their path. Here we show growth rate and stable isotope (18O, 13C) profiles from a South Island, New Zealand, stalagmite (HW3) that permit centennial-scale investigation of Southern Hemisphere westerly paleointensity between 73 and 11 ka. Correlation between HW3 growth rate and isotope profiles suggests sensitivity to changes in annual precipitation, a factor controlled by westerly intensity. Low growth rates and relatively enriched isotope ratios define long-term trends in HW3, supporting existing evidence that weaker westerlies predominated during the last glacial period. Abrupt millennial-scale events occur frequently, such that the HW3 record resembles Greenland ice core stable isotope profiles. Furthermore, nearly synchronous timing of nine prominent wet and cool intervals with Heinrich events supports studies showing that increased westerly intensity is closely linked to North Atlantic cooling. As well as Heinrich events, the HW3 profiles also show an Antarctic Cold Reversal–like event during deglaciation, advocating for a bipolar seesaw of global climate at that time.

year: 2011

title: Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts

authors: Britten, Daniel

subjects: software engineering

abstract: Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed.
Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract.
As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once (excluding any calls related to invoking other smart contracts). This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.

text: Using Coq to Enforce the Checks-Effects-Interactions Pattern in DeepSEA Smart Contracts Using the DeepSEA system for smart contract proofs, this paper investigates how to use the Coq theorem prover to enforce that smart contracts follow the Checks-Effects-Interactions Pattern. This pattern is widely understood to mitigate the risks associated with reentrancy. The infamous "The DAO" exploit is an example of the risks of not following the Checks-Effects-Interactions Pattern. It resulted in the loss of over 50 million USD and involved reentrancy - the exploit used would not have been possible if the Checks-Effects-Interactions Pattern had been followed.
Remix IDE, for example, already has a tool to check that the Checks-Effects-Interactions Pattern has been followed as part of the Solidity Static Analysis module which is available as a plugin. However, aside from simply replicating the Remix IDE feature, implementing a Checks-Effects-Interactions Pattern checker in the proof assistant Coq also allows us to use the proofs, which are generated in the process, in other proofs related to the smart contract.
As an example of this, we will demonstrate an idea for how the modelling of Ether transfer can be simplified by using automatically generated proofs of the property that each smart contract function will call the Ether transfer method at most once (excluding any calls related to invoking other smart contracts). This property is a consequence of following a strict version of the Checks-Effects-Interactions Pattern as given in this paper.

year: 2021

title: The discovery of the Waiorongomai goldfield in 1881

authors: Hart, Philip

abstract: The first reports of gold being found in the vicinity of the Waiorongomai Stream were made in early November 1880, and after the opening of the goldfield a small rush took place to this part of the mountain. The first claims were pegged out in December and the following January, encouraged by some gold being found, but few claims were registered, for most prospectors were quickly disappointed. Prospecting was difficult because of the rugged terrain and heavy bush, and interest quickly faded.
Then, in early October, Hone Werahiko announced his latest and best find and provided samples of payable ore taken from a large reef. Immense excitement ensued, as this was the first payable reef to be found, and after Werahiko led miners on an exhausting trip to his ‘New Find’ a rush set in and many claims were pegged out. The first official to inspect the ground anticipated that the reefs could be easily worked, once an access track was constructed. The small settlement of Te Aroha was revived because a real goldfield had been found, at last.

text: The discovery of the Waiorongomai goldfield in 1881 The first reports of gold being found in the vicinity of the Waiorongomai Stream were made in early November 1880, and after the opening of the goldfield a small rush took place to this part of the mountain. The first claims were pegged out in December and the following January, encouraged by some gold being found, but few claims were registered, for most prospectors were quickly disappointed. Prospecting was difficult because of the rugged terrain and heavy bush, and interest quickly faded.
Then, in early October, Hone Werahiko announced his latest and best find and provided samples of payable ore taken from a large reef. Immense excitement ensued, as this was the first payable reef to be found, and after Werahiko led miners on an exhausting trip to his ‘New Find’ a rush set in and many claims were pegged out. The first official to inspect the ground anticipated that the reefs could be easily worked, once an access track was constructed. The small settlement of Te Aroha was revived because a real goldfield had been found, at last.

year: 2016