Type-omega DPLs

Type-omega DPLs (Denotational Proof Languages) are languages for proof presentation and search that offer strong soundness guarantees. LCF-type systems such as HOL offer similar guarantees, but their soundness relies heavily on static type systems. By contrast, DPLs ensure soundness dynamically, through their evaluation semantics; no type system is necessary. This is possible owing to a novel two-tier syntax that separates deductions from computations, and to the abstraction of assumption bases, which is factored into the semantics of the language and allows for sound evaluation. Every type-omega DPL properly contains a type-alpha DPL, which can be used to present proofs in a lucid and detailed form, exclusively in terms of primitive inference rules. Derived inference rules are expressed as user-defined methods, which are "proof recipes" that take arguments and dynamically perform appropriate deductions. Methods arise naturally via parametric abstraction over type-alpha proofs. In that light, the evaluation of a method call can be viewed as a computation that carries out a type-alpha deduction. The type-alpha proof "unwound" by such a method call is called the "certificate" of the call. Certificates can be checked by exceptionally simple type-alpha interpreters, and thus they are useful whenever we wish to minimize our trusted base. Methods are statically closed over lexical environments, but dynamically scoped over assumption bases. They can take other methods as arguments, they can iterate, and they can branch conditionally. These capabilities, in tandem with the bifurcated syntax of type-omega DPLs and their dynamic assumption-base semantics, allow the user to define methods in a style that is disciplined enough to ensure soundness yet fluid enough to permit succinct and perspicuous expression of arbitrarily sophisticated derived inference rules. We demonstrate every major feature of type-omega DPLs by defining and studying NDL-omega, a higher-order, lexically scoped, call-by-value type-omega DPL for classical zero-order natural deduction---a simple choice that allows us to focus on type-omega syntax and semantics rather than on the subtleties of the underlying logic. We start by illustrating how type-alpha DPLs naturally lead to type-omega DPLs by way of abstraction; present the formal syntax and semantics of NDL-omega; prove several results about it, including soundness; give numerous examples of methods; point out connections to the lambda-phi calculus, a very general framework for type-omega DPLs; introduce a notion of computational and deductive cost; define several instrumented interpreters for computing such costs and for generating certificates; explore the use of type-omega DPLs as general programming languages; show that DPLs do not have to be type-less by formulating a static Hindley-Milner polymorphic type system for NDL-omega; discuss some idiosyncrasies of type-omega DPLs such as the potential divergence of proof checking; and compare type-omega DPLs to other approaches to proof presentation and discovery. Finally, a complete implementation of NDL-omega in SML-NJ is given for users who want to run the examples and experiment with the language.

Effects of Platinum on NiPtSiGe/n-SiGe and NiPtSi/n-Si Schottky Contacts

Solid phase reaction of NiPt/Si and NiPt/SiGe is one of the key issues for silicide (germanosilicide) technology. Especially, the NiPtSiGe, in which four elements are involved, is a very complex system. As a result, a detailed study is necessary for the interfacial reaction between NiPt alloy film and SiGe substrate. Besides using traditional material characterization techniques, characterization of Schottky diode is a good measure to detect the interface imperfections or defects, which are not easy to be found on large area blanket samples. The I-V characteristics of 10nm Ni(Pt=0, 5, 10 at.%) germanosilicides/n-Si₀/₇Ge₀.₃ and silicides/n-Si contact annealed at 400 and 500°C were studied. For Schottky contact on n-Si, with the addition of Pt in the Ni(Pt) alloy, the Schottky barrier height (SBH) increases greatly. With the inclusion of a 10% Pt, SBH increases ~0.13 eV. However, for the Schottky contacts on SiGe, with the addition of 10% Pt, the increase of SBH is only ~0.04eV. This is explained by pinning of the Fermi level. The forward I-V characteristics of 10nm Ni(Pt=0, 5, 10 at.%)SiGe/SiGe contacts annealed at 400°C were investigated in the temperature range from 93 to 300K. At higher temperature (>253K) and larger bias at low temperature (<253K), the I-V curves can be well explained by a thermionic emission model. At lower temperature, excess currents at lower forward bias region occur, which can be explained by recombination/generation or patches due to inhomogenity of SBH with pinch-off model or a combination of the above mechanisms.