Thesis (Ph.D.) OGI School of Science & Engineering at OHSU, May 2007. / Includes bibliographical references (leaves 323-338).

Η παρακάτω διπλωματική αφού κάνει μια εκτενή αναφορά στα είδη των γλωσσών προγραμματισμού επεκτείνεται και στην περιγραφή των frameworks που χρησιμοποιούνται σήμερα ευρέως. Έπειτα ασχολούμαστε εκτενώς με το framework ruby on rails και περιγράφουμε αναλυτικά τις δυνατότητες που μας προσφέρει μέσα από την ανάπτυξη κάποιων εφαρμογών. Ακριβέστερα, έχουν υλοποιηθεί και αξιολογηθεί ένα site με forum και shopping cart, ένα blog, μια wiki page και ένα site για δημιουργία προφίλ από τους χρήστες του. / The following work has made an extensive reference to the kinds of programming languages and then extends a description of the frameworks currently used widely. Then devotes considerable attention to the framework ruby on rails and describes in detail the possibilities offered by means of developing some applications. Being more specific, we implemented and evaluated a site with forum and shopping cart, a blog, a wiki page, and a site for creation profile of its users.

Intensionality is a phenomenon that occurs in logic and computation. In the most general sense, a function is intensional if it operates at a level finer than (extensional) equality. This is a familiar setting for computer scientists, who often study different programs or processes that are interchangeable, i.e. extensionally equal, even though they are not implemented in the same way, so intensionally distinct. Concomitant with intensionality is the phenomenon of intensional recursion, which refers to the ability of a program to have access to its own code. In computability theory, intensional recursion is enabled by Kleene's Second Recursion Theorem. This thesis is concerned with the crafting of a logical toolkit through which these phenomena can be studied. Our main contribution is a framework in which mathematical and computational constructions can be considered either extensionally, i.e. as abstract values, or intensionally, i.e. as fine-grained descriptions of their construction. Once this is achieved, it may be used to analyse intensional recursion. To begin, we turn to type theory. We construct a modal λ-calculus, called Intensional PCF, which supports non-functional operations at modal types. Moreover, by adding Löb's rule from provability logic to the calculus, we obtain a type-theoretic interpretation of intensional recursion. The combination of these two features is shown to be consistent through a confluence argument. Following that, we begin searching for a semantics for Intensional PCF. We argue that 1-category theory is not sufficient, and propose the use of P-categories instead. On top of this setting we introduce exposures, which are P-categorical structures that function as abstractions of well-behaved intensional devices. We produce three examples of these structures, based on Gödel numberings on Peano arithmetic, realizability theory, and homological algebra. The language of exposures leads us to a P-categorical analysis of intensional recursion, through the notion of intensional fixed points. This, in turn, leads to abstract analogues of classic intensional results in logic and computability, such as Gödel's Incompleteness Theorem, Tarski's Undefinability Theorem, and Rice's Theorem. We are thus led to the conclusion that exposures are a useful framework, which we propose as a solid basis for a theory of intensionality. In the final chapters of the thesis we employ exposures to endow Intensional PCF with an appropriate semantics. It transpires that, when interpreted in the P-category of assemblies on the PCA K1, the Löb rule can be interpreted as the type of Kleene's Second Recursion Theorem.

We study the interplay between dependent types and computational effects, two important areas of modern programming language research. On the one hand, dependent types underlie proof assistants such as Coq and functional programming languages such as Agda, Idris, and F*, providing programmers a means for encoding detailed specifications of program behaviour using types. On the other hand, computational effects, such as exceptions, nondeterminism, state, I/O, probability, etc., are integral to all widely-used programming languages, ranging from imperative languages, such as C, to functional languages, such as ML and Haskell. Separately, dependent types and computational effects both come with rigorous mathematical foundations, dependent types in the effect-free setting and computational effects in the simply typed setting. Their combination, however, has received much less attention and no similarly exhaustive theory has been developed. In this thesis we address this shortcoming by providing a comprehensive treatment of the combination of these two fields, and demonstrating that they admit a mathematically elegant and natural combination. Specifically, we develop a core effectful dependently typed language, eMLTT, based on Martin-L¨of’s intensional type theory and a clear separation between (effect-free) values and (possibly effectful) computations familiar from simply typed languages such as Levy’s Call-By-Push-Value and Egger et al.’s Enriched Effect Calculus. A novel feature of our language is the computational S-type, which we use to give a uniform treatment of type-dependency in sequential composition. In addition, we define and study a class of category-theoretic models, called fibred adjunction models, that are suitable for defining a sound and complete interpretation of eMLTT. Specifically, fibred adjunction models naturally combine standard category-theoretic models of dependent types (split closed comprehension categories) with those of computational effects (adjunctions). We discuss and study various examples of these models, including a domain-theoretic model so as to extend eMLTT with general recursion. We also investigate a dependently typed generalisation of the algebraic treatment of computational effects by showing how to extend eMLTT with fibred algebraic effects and their handlers. In particular, we specify fibred algebraic effects using a dependently typed generalisation of Plotkin and Pretnar’s effect theories, enabling us to capture precise notions of computation such as state with location-dependent store types and dependently typed update monads. For handlers, we observe that their conventional term-level definition leads to unsound program equivalences becoming derivable in languages that include a notion of homomorphism, such as eMLTT. To solve this problem, we propose a novel type-based treatment of handlers via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a family of value terms (the operations). This type internalises Plotkin and Pretnar’s insight that handlers denote algebras for a given equational theory of computational effects. We demonstrate the generality of our type-based treatment of handlers by showing that their conventional term-level presentation can be routinely derived, and this treatment provides a useful mechanism for reasoning about effectful computations. Finally, we show that these extensions of eMLTT can be soundly interpreted in a fibred adjunction model based on the families of sets fibration and models of Lawvere theories.

Education of programming language is often included in Czech secondary education as a method of implementation of corresponding school standards. By the time of publishing this thesis, these standards are only vaguely defined, so the effect of teaching programming can't be objectively evaluated from the perspective of the standards. This thesis elaborates on the usability of educational programming languages with respect to cognitive level of secondary school students, which may be used as a founded source in defining standards of particular schools.

Doctorat en Sciences / info:eu-repo/semantics/nonPublished

The goal of this thesis is to explore the current possibilities of implementation of compilers of low-level functional languages. It is expected to evaluate theoretical possibilities of functional programming languages, possible limitations that arise from the absence of run-time code support in low-level environment, and to implement a language compiler that demonstrates some chosen properties. Powered by TCPDF (www.tcpdf.org)

Viper is a verification infrastructure developed at ETH Zurich. Using this infrastructure, programs written in the Viper language may be analyzed for correctness with respect to assertions and contracts. In this thesis, we develop a contracts library and a translator program that compiles C# code into the Viper language and thus allows it to be verified. A user may annotate their C# program with these contracts and then use the translator to determine its functional correctness. The translator supports most C# features, including types and arrays. It also integrates with Visual Studio, showing translation and verification errors to the user on-the-fly.

The use of augmented transition network (ATM) gramaars for the analysis of natural language sentences is discussed. A small sample grammar is illustrated and briefly described. An ATN grammar for English was implemented and is described in detail. This grammar uses both semantic and syntactic information to guide the parsing. The value of the ATM model for natural language analysis is critically evaluated. / Science, Faculty of / Computer Science, Department of / Graduate

Considerable work has been recently devoted to the automatic generation of syntax analyzers. This work has been generally concerned with extending the power of the parser generator technigues, rather than improving the syntactic specification mechanism. Se present a new parsing language which attempts to unify syntax and semantics. In addition, the language provides a mechanism by which reasonable error recovery can be naturally included in the syntax specification. / Science, Faculty of / Computer Science, Department of / Graduate