LEGO is a computer program for interactive typechecking in the Extended Calculus of Constructions and two of its subsystems. LEGO also supports the extension of these three systems with inductive types. These type systems can be viewed as logics, and as meta languages for expressing logics, and LEGO is intended to be used for interactively constructing proofs in mathematical theories presented in these logics. I have developed LEGO over six years, starting from an implementation of the Calculus of Constructions by Gérard Huet. LEGO has been used for problems at the limits of our abilities to do formal mathematics. In this thesis I explain some aspects of the meta-theory of LEGO's type systems leading to a machine-checked proof that typechecking is decidable for all three type theories supported by LEGO, and to a verified algorithm for deciding their typing judgements, assuming only that they are normalizing. In order to do this, the theory of Pure Type Systems (PTS) is extended and formalized in LEGO. This extended example of a formally developed body of mathematics is described, both for its main theorems, and as a case study in formal mathematics. In many examples, I compare formal definitions and theorems with their informal counterparts, and with various alternative approaches, to study the meaning and use of mathematical language, and suggest clarifications in the informal usage. Having outlined a formal development far too large to be surveyed in detail by a human reader, I close with some thoughts on how the human mathematician's state of understanding and belief might be affected by possessing such a thing.

We present a type-based approach to statically derive symbolic closed-form formulae that characterize the bounds of heap memory usages of programs written in object-oriented languages. Given a program with size and alias annotations, our inference system will compute the amount of memory required by the methods to execute successfully as well as the amount of memory released when methods return. The obtained analysis results are useful for networked devices with limited computational resources as well as embedded software. / Singapore-MIT Alliance (SMA)

Security APIs are designed to enable the storage and processing of confidential data without that data becoming known to individuals who are not permitted to obtain it, and are central to the operation of Automated Teller Machines (ATM) networks, Electronic Point of Sale (EPOS) terminals, set-top boxes for subscription-based TV, pre-payment utility meters, and electronic ticketing for an increasing number of public transport systems (e.g., Oyster in London). However, since the early 2000s, it has become clear that many of the security APIs in widespread use contain subtle flaws which allow malicious individuals to subvert the security restrictions and obtain confidential data that should be protected. In this thesis, we attempt to address this problem by presenting a type system in which specific security properties are guaranteed to be enforced by security APIs that are well-typed. Since type-checking is a form of static analysis, it does not suffer from the scalability issues associated with approaches that simulate interactions between a security API and one or more malicious individuals. We also show how our type system can be used to model an existing security API and provide the same guarantees of security that the API authors proved it upholds. This result follows directly from producing a well-typed implementation of the API, and demonstrates how our type system provides security guarantees without requiring additional API-specific proofs.

Representing data outside of and between programs is important in software that stores, shares, and manipulates information. Formats for representing information, varying from human-readable verbose (XML) to light-weight, concise (JSON), and non-human-readable formats (TLV) have been developed and used by applications based on their data and communication requirements. Writing correct programs that produce information represented in these formats is a difficult and time-consuming task, as developers must write repetitive, tedious code to map loosely-typed serialized data to strongly-typed program objects. We developed S.IM.PL Serialization, a cross-language multi-format information binding framework to relieve developers from the burdens associated with the serialization of strongly-typed data structures. We developed type system scopes, a means of encapsulating data types and binding semantics as a cross-language abstract semantics graph. In comparison to representing data binding semantics and information structure through external forms such as schemas, configuration files, and interface description languages, type system scopes can be automatically generated from declarations in a data binding annotation language, facilitating software engineering. Validation is based on use in research applications, a study of how computer science graduate students use the software to develop applications, and performance benchmarks. As a case study, we also examine the cross-language development of a Team Coordination (TeC) game.

Master of Science / Department of Computing and Information Sciences / John M. Hatcliff / Guardol, a domain-specific language (DSL) developed by Rockwell Collins, was designed to streamline the process of specifying, implementing, and verifying Cross Domain Solution (CDS) security policies. Guardol’s syntax and intended computational behavior tightly resembles the core of many functional programming languages, but a number of features have been added to ease the development of high assurance cross domain solutions. A significant portion of the formalization and implementation of Guardol’s grammar and type system was performed by the SAnToS group at Kansas State University. This report summarizes the key conceptual components of Guardol’s grammar and tool- chain architecture. The focus of the report is a detailed description of Guardol’s type system implementation and formalization. A great deal of effort was put into a formalization which provided a high level of assurance that the specification of types and data structures were maintained in the intended implementation.

The humanitarian sector is in need to prioritize its human resources. Inadequate recruitment processes, aid workers that enter the field unprepared, failed interrelationships and team dissatisfaction leads to poorer work quality, poorer health, and a high employee turnover that are costly for the field, and negative on the side of accountability to the beneficiaries of aid. In order to address these problems the study is investigating the use of a personality type system tool developed by the researcher, the 4mpt-system (4 major personality types-system),that tentatively is constructed as a tool to be applied within human resources in the humanitarian sector to access individual preferences and character traits that would facilitate in addressing the issues mentioned above. The data is gathered via in-depth semi-structured interviews of 7 informants working in the international humanitarian sector. The first objective is to study the reliability and validity of the 4mpt-system. The second objective is to study what information that could be accessed via the 4mpt-system tool from the 7 informants participating in the study. The result of the study would demonstrate that all of the informants could be assigned to a specific temperament type via a qualitative data analyze method designed from the 4mpt-system and that the temperaments affected the informants to a large extent (from motivations and skills to organisational preferences and personal belief systems). Further, the answers of the informants matched the theoretical definitions of the traits assigned to the temperament types by Keirsey (1998) and Fisher (2009), which was a positive indication for a good validity of the 4mpt-system. By verifying the similarity between the answers of informants assigned to the same temperament type, validity was further confirmed. The results of the study supported the reliability and validity of the 4mpt -system. The type of information that could be accessed via the 4mpt-system in the study was among other the motivation for beginning in the humanitarian field, work task preferences, professional skills, problem-solving approaches, decision making processes, likes and dislikes with work and work tasks, organisational structure preference, preference for working directly in the field or working from the office, and general outlooks and personal belief systems.

One of the most difficult tasks a programmer can be confronted with is the migration of a legacy system. Usually, these systems are unstructured, poorly documented and contain complex program logic. The reason for this, in most cases, is an emphasis on raw performance rather than on clean and structured code as well as a long period of applying quick fixes and enhancements rather than doing a proper software reengineering process including a full redesign during major enhancements. Nowadays, the old programming paradigms are becoming an increasingly serious problem. It has been identified that 90% of the costs of a typical software system arise in the maintenance phase. Many companies are simply too afraid of changing their software infrastructure and prefer to continue with principles like "never touch a running system". These companies experience growing pressure to migrate their legacy systems onto newer platforms because the maintenance of such systems is expensive and dangerous as the risk of losing vital parts of sources code or its documentation increases drastically over time. The FermaT transformation system has shown the ability to automatically or semi-automatically restructure and abstract legacy code within a special intermediate language called WSL (Wide Spectrum Language). Unfortunately, the current transformation process only supports the migration of assembler as WSL lacks the ability to handle data types properly. The data structures in assembler are currently directly translated into C data types which involves many assumptional “hard coded” conversions. The absence of an adequate type system for WSL caused several flaws for the whole transformation process and limits its abilities significantly. The main aim of the presented research is to tackle these problems by investigating and formulating how a type system can contribute to a safe and reliable migration of legacy systems. The described research includes the definition of key aspects of type related problems in the FermaT migration process and how to solve them with a suitable type system approach. Since software migration often includes a change in programming language the type system for WSL has to be able to support various type system approaches including the representation of all relevant details to avoid assumptions. This is especially difficult as most programming languages are designed for a special purpose which means that their possible programming constructs and data types differ significantly. This ranges from languages with simple type systems whose program sare prone to unintended side-effects, to languages with strict type systems which are constrained n their flexibility. It is important to include as many type related details as necessary to avoid making assumptions during language to language translation. The result of the investigation is a novel multi layered type system specifically designed to satisfy the needs of WSL for a sophisticated solution without imposing too many limitations on its abilities. The type system has an adjustable expressiveness, able to represent a wide spectrum of typing approaches ranging from weak typing which allows direct memory access and down casting, via very strict typing with a high diversity of data types to object oriented typing which supports encapsulation and data hiding. Looking at the majority of commercial relevant statically typed programming languages, two fundamental properties of type strictness and safety can be identified. A type system can be either weakly or strongly typed and may or may not allow unsafe features such as direct memory access. Each layer of the Wide Spectrum Type System has a different combination of these properties. The approach also includes special Type System Transformations which can be used to move a given WSL program among these layers. Other emphasised key features are explicit typing and scalability. The whole approach is based on a sound mathematical foundation which assures correctness and integrates seamlessly into the present mathematical definition of WSL. The type system is formally introduced to WSL by constructing an attribute grammar for the language. Type checking and type inference are used to annotate the Abstract Syntax Tree of a given WSL program with type derivations which can be used to reveal and indicate possible typing errors or to infer types if the program did not feature explicit type declarations in the first place. Notable in this approach is also the fact that object orientation is introduced to a procedural programming language without the introduction of new semantics. It is shown that object orientation can be introduced just by adjusting type checking rules and adding some syntactical notations. The approach was implemented and tested on two case studies. The thesis describes and discusses both cases in detail and shows how a migration which ignores type systems could accidentally introduce errors due to assumptions during translation. Both case studies use all important aspects of the approach, Including type transformations and object identification. The thesis finalises by summarising the whole work, identifying limitations, presenting future perspectives and drawing conclusions

Interference makes reasoning about imperative programs difficult but it can be controlled syntactically by a language's type system, such as Syntactic Control of Interference (SCI). Haskell is a purely-functional, statically-typed language with a rich type system including algebraic datatypes and type classes. It is popular as a defining language for definitional interpreters of domain-specific languages, making it an ideal candidate for implementation of definitional interpreters for SCI and Syntactic Control of Interference Revisited (SCIR), a variant that improves on SCI. Inference rules and denotational semantics functions are presented for PCF, IA, SCI, and SCIR. An extension to Haskell98 is used to define Haskell functions for those languages' semantics and to define type constructions to statically check their syntax. The results in applied programming language theory demonstrate the suitability and techniques of Haskell for definitional interpretation of languages with rich type systems. / Thesis (Master, Computing) -- Queen's University, 2008-06-10 21:23:33.291

Type checking is widely used in mainstream programming languages to detect programming errors at compile time. Model checking is gaining popularity as an automated technique for systematically analyzing behaviors of systems. My research focuses on combining these two software verification techniques synergically into one platform for the creation of correct models for software designs. This thesis describes two modeling languages ATS/PML and ATS/Veri that inherit the advanced type system from an existing programming language ATS, in which both dependent types of Dependent ML style and linear types are supported. A detailed discussion is given for the usage of advanced types to detect modeling errors at the stage of model construction. Going further, various modeling primitives with well-designed types are introduced into my modeling languages to facilitate a synergic combination of type checking with model checking. The semantics of ATS/PML is designed to be directly rooted in a well-known modeling language PROMELA. Rules for translation from ATS/PML to PROMELA are designed and a compiler is developed accordingly so that the SPIN model checker can be readily employed to perform checking on models constructed in ATS/PML. ATS/Veri is designed to be a modeling language, which allows a programmer to construct models for real-world multi-threaded software applications in the same way as writing a functional program with support for synchronization, communication, and scheduling among threads. Semantics of ATS/Veri is formally defined for the development of corresponding model checkers and a compiler is built to translate ATS/Veri into CSP# and exploit the state-of-the-art verification platform PAT for model checking ATS/Veri models. The correctness of such a transformational approach is illustrated based on the semantics of ATS/Veri and CSP#. In summary, the primary contribution of this thesis lies in the creation of a family of modeling languages with highly expressive types for modeling concurrent software systems as well as the related platform supporting verification via model checking. As such, we can combine type checking and model checking synergically to ensure software correctness with high confidence.

付記する学位プログラム名: デザイン学大学院連携プログラム / 京都大学 / 0048 / 新制・課程博士 / 博士(情報学) / 甲第21217号 / 情博第670号 / 新制||情||115(附属図書館) / 京都大学大学院情報学研究科通信情報システム専攻 / (主査)教授 五十嵐 淳, 教授 石田 亨, 教授 山本 章博 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM