Essays about: "agda"

Showing result 1 - 5 of 12 essays containing the word agda.

  1. 1. Agda on Raspberry Pi

    University essay from Göteborgs universitet/Institutionen för data- och informationsteknik

    Author : Lawerence Chonavel; [2023-10-25]
    Keywords : Agda; Compiler; Raspbery Pi; Functional Programming; BUBS;

    Abstract : This thesis presents an Agda-to-C compiler targeting the Raspberry Pi Pico microcontroller. The compiler implementation includes an unusual choice of run-time algorithm, a Foreign Function Interface generator, and surprisingly little boilerplate code... READ MORE

  3. 2. Understanding Gender Equal Conflict Resolution – A Sociology of Law Perspective of Inclusive Education as One Pathway to Sustainable Peacebuilding

    University essay from Lunds universitet/Rättssociologiska institutionen

    Author : Michelle Gano; [2023]
    Keywords : gender equality; education; girls; conflict resolution; peacebuilding; global security; peace negotiation; peace processes; legal empowerment; legal feminism; legal security feminism; Law and Political Science; Social Sciences;

    Abstract : The significance of access to education has, like women’s role in peacebuilding, previously been examined in various studies. However, the relationship between these two has rarely been touched upon. Particularly the discipline of Sociology of Law has been observed to discuss the topics in separate academic discussions. READ MORE

  4. 3. An Arrow Metalanguage for Partially Invertible Computation

    University essay from KTH/Skolan för elektroteknik och datavetenskap (EECS)

    Author : Anders Ågren Thuné; [2023]
    Keywords : Reversible computation; Domain-specific languages; Arrows; Partial invertibility; Reversibel beräkning; Domänspecifika språk; Arrows; Partiell inverterbarhet;

    Abstract : Programming languages traditionally describe computations going one way: a program might compute a hash value from a string, or an encrypted message from a plaintext. However, sometimes it is also of interest to go the other way around: for encryption, we not only want to encrypt messages but also to decrypt them, and to be sure that the decryption correctly reproduces the original message. READ MORE

  5. 4. Formalisation of Polynomials in Cubical Type Theory Using Cubical Agda

    University essay from Stockholms universitet/Matematiska institutionen

    Author : Carl Åkerman Rydbeck; [2022]
    Keywords : ;

    Abstract : We formalise polynomials over commutative rings in cubical type theory using Cubical Agda as proof assistant. On the basis of a formalisation of polynomials as number sequences with only a finite number of non-zero values, we use higher inductive types to formulate a list-based definition using two point constructors and two path constructors. READ MORE

  6. 5. Formalizing domain models of the typed and the untyped lambda calculus in Agda

    University essay from Göteborgs universitet/Institutionen för data- och informationsteknik

    Author : David Lidell; [2020-12-17]
    Keywords : Agda; categories with families; domain interpretation; lambda calculus; sized types;

    Abstract : We present a domain interpretation of the simply typed and the untyped lambda calculus. The interpretations are constructed using the notion of category with families, with added structure. READ MORE