Sökning: "Lambda Calculus"

Visar resultat 6 - 10 av 12 avhandlingar innehållade orden Lambda Calculus.

1. 6. Psi-calculi: a framework for mobile process calculi : Cook your own correct process calculus - just add data and logic

   Författare :Magnus Johansson; Björn Victor; Joachim Parrow; Catuscia Palamidessi; Uppsala universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; process calculi; pi-calculus; bisimulation; operational semantics; nominal logic; Computer science; Datavetenskap; Datavetenskap; Computer Science;

   Sammanfattning : A psi-calculus is an extension of the pi-calculus with nominal data types for data structures, logical assertions, and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. LÄS MER

3. 7. Primitive Direcursion and Difunctorial Semantics of Typed Object Calculus

   Författare :Johan Glimming; Karl Meinke; John Power; Stockholms universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; denotational semantics; axiomatic domain theory; coalgebra; primitive co recursion; object-based programming; typed object calculus; Computer science; Datavetenskap; datalogi; Computer Science;

   Sammanfattning : In the first part of this thesis, we contribute to the semantics of typed object calculus by giving (a) a category-theoretic denotational semantics using partial maps making use of an algebraic compactness assumption, (b) a notion of "wrappers'' by which algebraic datatypes can be represented as object types, and (c) proofs of computational soundness and adequacy of typed object calculus via Plotkin's FPC (with lazy operational semantics), thus making models of FPC suitable also for first-order typed object calculus (with recursive objects supporting method update, but not subtyping). It follows that a valid equation in the model induces operationally congruent terms in the language, so that program algebras can be studied. LÄS MER

4. 8. Testing and Proving in Dependent Type Theory

   Författare :Qiao Haiyan; Chalmers tekniska högskola; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES;

   Sammanfattning : We show how random testing, model checking and interactive proving can be combined for functional program verification in dependent type theory. We extend the proof assistant Agda/Alfa for dependent type theory with a tool for random testing of functional programs, thus combining proving and testing in one system. LÄS MER

5. 9. Safety, Security, and Semantic Aspects of Equation-Based Object-Oriented Languages and Environments

   Författare :David Broman; Peter Fritzson; Henrik Nilsson; Linköpings universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Modeling; Simulation; Equation-Based; Object-Oriented; Modelica; Type System; Semantics; Language Safety; Secure Simulation; Computer science; Datavetenskap;

   Sammanfattning : During the last two decades, the interest for computer aided modeling and simulation of complex physical systems has witnessed a significant growth. The recent possibility to create acausal models, using components from different domains (e.g., electrical, mechanical, and hydraulic) enables new opportunities. LÄS MER

7. 10. Meta-Languages and Semantics for Equation-Based Modeling and Simulation

   Författare :David Broman; Peter Fritzson; Jeremy Siek; Thomas Schön; Björn Lisper; Walid Taha; Linköpings universitet; []
   Nyckelord :NATURVETENSKAP; NATURAL SCIENCES; Meta-language; semantics; EOO; Modelica; equations; modeling; simulation; MKL; Computer science; Datalogi;

   Sammanfattning : Performing computational experiments on mathematical models instead of building and testing physical prototypes can drastically reduce the develop cost for complex systems such as automobiles, aircraft, and powerplants. In the past three decades, a new category of equation-based modeling languages has appeared that is based on acausal and object-oriented modeling principles, enabling good reuse of models. LÄS MER