title: Investigating the interhemispheric ¹⁴C offset in the 1st millennium AD and assessment of laboratory bias and calibration errors

authors: Hogg, Alan G.

subjects: radiocarbon

abstract: Past measurements of the radiocarbon interhemispheric offset have been restricted to relatively young samples because of a lack of older dendrochronologically secure Southern Hemisphere tree-ring chronologies. The Southern Hemisphere calibration data set SHCal04 earlier than AD 950 utilizes a variable interhemispheric offset derived from measured 2nd millennium AD Southern Hemisphere/Northern Hemisphere sample pairs with the assumption of stable Holocene ocean/atmosphere interactions. This study extends the range of measured interhemispheric offset values with 20 decadal New Zealand kauri and Irish oak sample pairs from 3 selected time intervals in the 1st millennium AD and is part of a larger program to obtain high-precision Southern Hemisphere 14C data continuously back to 200 BC. We found an average interhemispheric offset of 35 ± 6 yr, which although consistent with previously published 2nd millennium AD measurements, is lower than the offset of 55–58 yr utilized in SHCal04. We concur with McCormac et al. (2008) that the IntCal04 measurement for AD 775 may indeed be slightly too old but also suggest the McCormac results appear excessively young for the interval AD 755–785. In addition, we raise the issue of laboratory bias and calibration errors, and encourage all laboratories to check their consistency with appropriate calibration curves and invest more effort into improving the accuracy of those curves.

text: Investigating the interhemispheric ¹⁴C offset in the 1st millennium AD and assessment of laboratory bias and calibration errors Past measurements of the radiocarbon interhemispheric offset have been restricted to relatively young samples because of a lack of older dendrochronologically secure Southern Hemisphere tree-ring chronologies. The Southern Hemisphere calibration data set SHCal04 earlier than AD 950 utilizes a variable interhemispheric offset derived from measured 2nd millennium AD Southern Hemisphere/Northern Hemisphere sample pairs with the assumption of stable Holocene ocean/atmosphere interactions. This study extends the range of measured interhemispheric offset values with 20 decadal New Zealand kauri and Irish oak sample pairs from 3 selected time intervals in the 1st millennium AD and is part of a larger program to obtain high-precision Southern Hemisphere 14C data continuously back to 200 BC. We found an average interhemispheric offset of 35 ± 6 yr, which although consistent with previously published 2nd millennium AD measurements, is lower than the offset of 55–58 yr utilized in SHCal04. We concur with McCormac et al. (2008) that the IntCal04 measurement for AD 775 may indeed be slightly too old but also suggest the McCormac results appear excessively young for the interval AD 755–785. In addition, we raise the issue of laboratory bias and calibration errors, and encourage all laboratories to check their consistency with appropriate calibration curves and invest more effort into improving the accuracy of those curves.

year: 2009

title: Building trustworthy smart contracts using interactive theorem proving

authors: Britten, Daniel

subjects: formal methods

abstract: There are varying approaches to the verification of smart contracts using formal methods. This thesis advocates for the use of high-level specifications coupled with a verified compiler to low-level bytecode, such as for the Ethereum Virtual Machine. Taking this approach allows for specifications to more closely match natural language, while ensuring that the specifications apply to the real bytecode executed on-chain.

Interactive theorem proving can provide the foundation for developing provably correct smart contracts. Due to the immutable nature of smart contracts and their potential to manage highly valuable assets and tokens representing power, techniques to ensure their correctness are of paramount importance.

This thesis extends the DeepSEA (Deep Simulation of Executable Abstractions) smart contract language targeting the Ethereum Virtual Machine by mitigating the issues associated with reentrancy and introducing a model of relevant aspects of a blockchain. This enables the specification and verification of two case studies which exemplify the approach of developing provably correct smart contracts.

The specifications for the case studies are written in the language of the Coq Proof Assistant, making arbitrary mathematical statements expressible. The blockchain model enables stating and proving temporal properties relating to the execution of smart contract over time.

While smart contracts are an ideal application area for formal methods in general and interactive theorem proving in particular, the techniques exemplified in this thesis could be applied throughout software engineering. The relatively young age of smart contract languages and typically small size of smart contract programs makes the application of interactive theorem proving more tractable. Future work could involve demonstrating the applicability to many interrelated smart contracts and to larger software projects in different domains.

The first three chapters of this thesis cover introductory and background material. This is followed by the contributions to the DeepSEA system. The two case studies and the proof themes arising from them are then presented. Finally, concluding remarks and future work are discussed.

text: Building trustworthy smart contracts using interactive theorem proving There are varying approaches to the verification of smart contracts using formal methods. This thesis advocates for the use of high-level specifications coupled with a verified compiler to low-level bytecode, such as for the Ethereum Virtual Machine. Taking this approach allows for specifications to more closely match natural language, while ensuring that the specifications apply to the real bytecode executed on-chain.

Interactive theorem proving can provide the foundation for developing provably correct smart contracts. Due to the immutable nature of smart contracts and their potential to manage highly valuable assets and tokens representing power, techniques to ensure their correctness are of paramount importance.

This thesis extends the DeepSEA (Deep Simulation of Executable Abstractions) smart contract language targeting the Ethereum Virtual Machine by mitigating the issues associated with reentrancy and introducing a model of relevant aspects of a blockchain. This enables the specification and verification of two case studies which exemplify the approach of developing provably correct smart contracts.

The specifications for the case studies are written in the language of the Coq Proof Assistant, making arbitrary mathematical statements expressible. The blockchain model enables stating and proving temporal properties relating to the execution of smart contract over time.

While smart contracts are an ideal application area for formal methods in general and interactive theorem proving in particular, the techniques exemplified in this thesis could be applied throughout software engineering. The relatively young age of smart contract languages and typically small size of smart contract programs makes the application of interactive theorem proving more tractable. Future work could involve demonstrating the applicability to many interrelated smart contracts and to larger software projects in different domains.

The first three chapters of this thesis cover introductory and background material. This is followed by the contributions to the DeepSEA system. The two case studies and the proof themes arising from them are then presented. Finally, concluding remarks and future work are discussed.

year: 2024

title: Promoting social and environmental justice to support Indigenous partnerships in urban ecosystem restoration

authors: Hall, Monique

subjects: Science & Technology

abstract: Urban ecological restoration typically employs western science approaches to restore degraded ecosystems. As yet, few restoration groups acknowledge the history of these degraded urban sites, despite connections, past and present, that root Indigenous Peoples (and others) in these lands. Here, we promote partnership with Indigenous communities from project inception and present two successful case studies from Aotearoa New Zealand. We specifically note that partnering and building relationships with Indigenous communities in restoration efforts require recognition of power inequalities and injustices. We consider success to include both restoration of ecological function and biodiversity and reconnection of all communities to urban ecosystems.

text: Promoting social and environmental justice to support Indigenous partnerships in urban ecosystem restoration Urban ecological restoration typically employs western science approaches to restore degraded ecosystems. As yet, few restoration groups acknowledge the history of these degraded urban sites, despite connections, past and present, that root Indigenous Peoples (and others) in these lands. Here, we promote partnership with Indigenous communities from project inception and present two successful case studies from Aotearoa New Zealand. We specifically note that partnering and building relationships with Indigenous communities in restoration efforts require recognition of power inequalities and injustices. We consider success to include both restoration of ecological function and biodiversity and reconnection of all communities to urban ecosystems.

year: 2020-11-27