This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery. / Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinatoriska algebror—för varje partiell kombinatorisk algebra finns det en motsvarande realiserbarhetstolkning. Jag konstruerar två partiella kombinatoriska algebror. En av dessa ger en realiserbarhetstolkning som är ekvivalent med Kleenes ursprungliga tolkning, men dess konstruktion använder inte det sedvanliga rekursionsteoretiska maskineriet.

The currently available tools to simulate solar photovoltaic (PV) systems do not offer a reliable solution to simulate string or module level inverter systems with partial shading and modules with mismatching electrical characteristics. The available methodologies to simulate this satisfying require computational power that is not commonly available. To make it possible to simulate these kinds of systems a methodology based around the software “System Advisory Model” (SAM) is proposed. The methodology assumes that shading is binary, meaning a module can either be fully shaded or not shaded at all. Two different global IV curve models are presented and evaluated in comparison with a more detailed Matlab global IV model based on the one diode equivalent circuit. All these methodologies disregards the impact of the bypass diodes in the PV module and this is considered a significant error, which has to be quantified. It is proposed that this should be done by using the two-diode equivalent circuit instead of the one diode model. Finally the methodology is not concluded to be reliable until verified in comparison with real world data. / De för närvarande tillgängliga simuleringsverktygen för solcellssystem erbjuder inte en tillförlitlig metod för simulering av delvis skuggade system eller system med moduler med olika elektriska egenskaper. De metoder som är tillgängliga för att simulera detta tillförlitligt kräver datorkraft som inte är allmäntillgänglig. För att göra det möjligt att simulera dessa typer av system föreslås en metod baserad kring programvaran "System Advisory Model" (SAM). Metoden utgår från antagandet att skuggning är binärt, vilket innebär att en modul kan antingen vara helt skuggad eller inte skuggad alls. Två olika globala IV-modeller presenteras och utvärderas i jämförelse med en detaljerad Matlab global IV-modell baserad på enkel-diods ekvivalenta kretsen. Denna metod bortser dock från effekterna av bypass-dioderna i PV-modulen och detta antas medföra betydande fel som måste kvantifieras, detta bör då göras med hjälp av två-diods ekvivalenta kretsen. Slutligen så kan metoden inte anses pålitlig förrän den har blivit verifierad med verkliga data.

Uppsatsen undersöker den spontana organisering genom informella nätverk som blev ett betydande inslag i Sveriges flyktingmottagande 2015. Utifrån en fallstudie av volontärer som är aktiva i organisationerna undersöker studien vilka motiv som ligger till grund för deras val att engagera sig utanför redan befintliga organisationer. Det huvudsakliga syftet med undersökningen är att studera huruvida den spontana formen av organisering bör betraktas som en ny social rörelse. Uppsatsens teoretiska ramverk utgår från teorier om hur sociala rörelser uppstår samt vad som utmärker mindre formell form av organisering. Sammanlagt genomfördes sju stycken semistrukturerade intervjuer med volontärer från organisationer registrerade i Sverige och som startade under flyktingmottagandet 2015. Bland organisationerna finns de med fokus på mottagandet i Sverige samt de med primärt internationellt fokus. Resultatet visar att volontärernas engagemang i den nya formen av organisering till stor del kan betraktas som en ny social rörelse med hänvisning till uppsatsens teoretiska ramverk.

Nitrogen and phosphorus pollution is still a serious environmental problem and a major threat to sustainable development, as they mainly cause eutrophication. Therefore, increasingly stricter requirements are placed on wastewater treatment plants when it comes to emissions of nutrients. To meet these requirements, it is important to continuously renew and improve the purification processes, thereby reducing the emissions of nutrients to the sea, lakes, and streams. The effect of simultaneous nitrogen removal and phosphorus recycling was investigated in this study, employing a one-step process for partial nitritation/anammox-hydroxyapatite (PN/HAP). An experiment in a laboratory-scale SBR reactor (Sequence Batch Reactor) was performed using wastewater from the side-stream centrate. This study validated results to a certain extent published studies by other researchers. However, they had almost exclusively used synthetic wastewater, unlike the here presented where real wastewater was used. The innovative PN/A-HAP process showed effective nitrogen and phosphorus removal without additional aeration or pH adjustment, which means lower energy consumption, reduced nitrous oxide emissions, and reduced sludge production. The results showed an average nitrogen removal efficiency of 32.84% and an average phosphorus removal efficiency of 71.48%. These results indicate significant potential for sustainable wastewater management for some nitrogen and phosphorus side streams at the treatment plants. However, further research is required on a larger scale to precisely assess the long-term separation efficiency for nitrogen and phosphorus, as well as the scalability and usability of the process under real conditions.  This Thesis was performed in the frame of a research project 'Process development of CA-induced HAP (Hydroxyapatite) granulation in nitrogen separation with Anammox' funded by the VA Cluster Mälardalen. / Kväve- och fosforföroreningar är fortfarande ett allvarligt miljöproblem och ett stort hot mot en hållbar utveckling, eftersom de främst orsakar övergödning. Därför ställs allt strängare krav på avloppsreningsverken när det gäller utsläpp av näringsämnen. För att uppfylla dessa strängare krav är det viktigt att kontinuerligt förnya och förbättra reningsprocesserna och därigenom minska utsläppen av näringsämnen till hav, sjöar och vattendrag. I denna studie undersöktes effekten av samtidig kväveavskiljning och fosforåtervinning från avloppsvatten med hjälp av en enstegsprocess för partiell nitritering/Anammox-Hydroxyapatit (PN/HAP). Ett experiment i laboratorieskala genomfördes med hjälp av en SBR-reaktor (sequence batch reactor) för behandling av avloppsvatten från sidoströmscentrat. Denna studie validerade delvis resultat från andra forskares publicerade studier.Dessa hade dock nästan uteslutande använt syntetiskt avloppsvatten till skillnad från den här presenterade där riktigt avloppsvatten användes. Den innovativa PN/A-HAP-processen visade effektiv kväve- och fosforavskiljning utan behov av ytterligare luftning eller pH-justering, vilket i praktiken betyder lägre energiförbrukning, minskade lustgasutsläpp och minskad slamproduktion. Resultaten visade en genomsnittlig kväveavskiljningseffektivitet på 32,84% och en genomsnittlig fosforavskiljningseffektivitet på 71,48%. Dessa resultat tyder på en betydande potential för hållbar avloppsvattenhantering för vissa kväve- och fosforrika sidoströmmar vid reningsverken. Det krävs dock ytterligare forskning i större skala för att exakt kunna bedöma den långsiktiga avskiljningseffektiviteten för kväve och fosfor, samt processens skalbarhet och användbarhet under verkliga förhållanden. Denna artikel är skriven som en del av ett forskningsprojekt 'Processutveckling av Ca-inducerad HAP (hydroxyapatit) granulering vid kväveavskiljning med anammox' finansierat av VA-kluster Mälardalen.

Syftet med denna uppsats är att undersöka vad som händer med vänskap på Facebook. En utgångspunkt i undersökningen är presentation av relevanta teorier om vänskap som jämförs med resultat av intervjuer med fem personer som är Facebookanvändare. Semistrukturerade intervjuer används som en kvalitativ ansats för att genomföra undersökningen. Undersökningens teoriunderlag består bl.a. utav redogörelsen av teorier om vänskap, ”aktivitetsfokus”, mångfalden av vänskap, vänskapsmekanismer, samt nätverk, organisation och partiell organisation. Facebook är ett snabbt växande socialt medium med fler än 500 miljoner registrerade användare över hela världen. Det intressanta är om vänskapens innehåll och mening förblir samma som vi upplevde det innan Facebook. Präglar Facebook som en social nätgemenskap våra vänskapsrelationer idag? Det är svårt att definiera vänskap. Intervjuerna har visat att vi fortfarande tänker på våra bästa vänner som de som alltid finns där när man behöver dem. En vänskap är sann, äkta, verklig och riktig. Enligt intervjuresultat ser man att alla vänner på Facebookvänskapslistor inte kan kallas för vänner egentligen. De är uppdelade i följande grupper som bekanta, ”yttre bekanta”, kollegor, släkt och gamla klasskompisar t ex. Man kan få nya vänner på Facebook, men då handlar det om ett gemensamt intresse eller en aktivitet som är substansen till den nya vänskapsrelationen. Undersökningens resultat har visat att man ofta blir vän på Facebook även med t ex sina vänners vänner. Detta är ett beteende som avviker från vänskapsteorin. Enligt vänskapsteorin behöver vi inte vara vänner med våra vänners vänner. Undersökningens slutsats är att alla intervjupersonerna upplever att deras vänskapsrelationer på Facebook inte har förändrats eller har möjligtvis blivit bättre. Det är tydligt att man upplever att Facebook underlättar kommunikation med vänner. Man har känslan av att ha sina vänner nära hela tiden pga. Facebook. Men sina bästa vänner kontaktar man ofta på ett annat sätt, dvs. via telefon eller träffar.

FPGAs are commonly used in cloud computing due to their ability  to be  programmed  as a processor that serves a specific purpose; hence, achieving high performance at low power. On the other hand, FPGAs have a lot of resources available, which are wasted if they host a single application or serve a single user’s request. Partially Reconfiguration technology enables FPGAs to divide their resources into different regions and then dynamically reprogram those regions with various applications during runtime. Therefore, they are considered as a good solution to eliminate the underutilization resource problem. Nevertheless, the sizes of these regions are static; they cannot be increased or decreased once they are defined. Thereby, it leads to the underutilization of reconfigurable region resources. This thesis addresses this problem, i.e., how to dynamically increase/decrease partially reconfigurable FPGA resources matching an application’s needs. Our solution enables expanding and contracting the FPGA resources allocated to an application by 1) application acceleration requirements expressed in multiple smaller modules which are configured into multiple reconfigurable regions assigned to the application dynamically  and 2) providing a low - area - overhead, configurable, and isolated communication mechanism by adjusting crossbar interconnect and WISHBONE interface among those multiple reconfigurable regions. / FPGA - kretsar har en förmåga  att programmeras som processorer med ett specifikt syfte vilket gör att de ofta används i molnlösningar. Det tager hög prestanda med låg effektförbrukning. Å andra sidan disponerar FPGA - kretsar över stora resurser, vilka är bortkastade om de enbart används av en applikation eller endast på en användares förfrågan. Partiellt omkonfigurerbara teknologier tillåter FPGA - kretsar att fördela resurser mellan olika regioner, och sen dynamiskt omprogrammera regioner med olika applikationer vid körning. Därför betraktas partiellt omkonfigurerbara teknologier som en bra lösning för att minimera underutnyttjande av resurser. Storleken på regionerna är statiska och kan inte ändras när de väl definierats, vilket leder till underutnyttjande av de omkonfigurerbara regionernas resurser. Denna uppsats angriper problemet med dynamisk allokering av partiellt omkonfigurerbara FPGA - resurser utifrån applikationens behov. Vår lösning möjliggör ökning och minskning av FPGA - resurser allokerade till en applikation genom 1) accelerering av applikationen genom att applikationen tilldelas flera mindre moduler konfigurerade till dynamiskt omkonfigurerbara regioner, och 2) tillhanda hållande av en effektiv konfigurerbar och isolerad kommunikationsmekanism, genom justering av crossbar - sammankoppling en  och  WISHBONE - gränssnittet hos de omkonfigurerbara regionerna.

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. In an invertible programming language, a single program specifies two directions of a transformation, and the language guarantees that the two correspond as inverses. Invertible languages often require programs to be composed from atomic invertible fragments, a property known as local invertibility. This requirement has connections to applications such as low-energy and quantum computing. However, many invertible algorithms are more naturally expressed as depending unidirectionally on some inputs, e.g., the encryption key—this property is known as partial invertibility. Existing work largely lacks a systematic treatment of partial invertibility, and the connection to the locally invertible paradigm is not yet well-understood. In this thesis, we show that with the right design tradeoff, partial invertibility can be expressed within a locally invertible setting. We present KALPIS, a new functional language supporting expressive partial invertibility, yet maintaining a straightforward locally invertible semantics. This is made formal by a novel arrow combinator language RRARR, with primitives embodying functions, parameterized bijections, and interactions between the two. The formulation is based on recent work on effects in invertible computation, namely the irreversibility effect and the reversible reader. We substantiate the work with a prototype implementation of KALPIS, and demonstrate its utility through a number of nontrivial examples. Further, we give a complete formalization of the two systems, including the operational semantics and type system of KALPIS and a locally invertible interpretation and equational characterization of RRARR. Finally, we give a compositional translation from KALPIS into RRARR, motivating us to call it an arrow metalanguage. Most of the formalization is mechanized using the proof assistant Agda. / Programmeringsspråk beskriver traditionellt beräkningar som går åt ett håll: ett program kan till exempel beräkna ett hash-värde från en sträng eller ett krypterat meddelande från en klartext. Ibland är det dock även av intresse att gå åt andra hållet: vid kryptering vill vi inte bara kryptera meddelanden utan också avkryptera dem, och vara säkra på att avkrypteringen korrekt återskapar det ursprungliga meddelandet. I ett inverterbart programmeringsspråk beskriver ett enskilt program två riktningar av en transformation, och språket garanterar att de två motsvarar varandra som inverser. Inverterbara språk kräver ofta att program konstrueras från enskilt inverterbara komponenter, en egenskap som kallas lokal inverterbarhet. Denna egenskap har kopplingar till tillämpningar som lågenergioch kvantdatorer. Å andra sidan är det ofta naturligt att inverterbara algoritmer beror enkelriktat på vissa indata, till exempel krypteringsnyckeln—något som kallas partiell inverbarhet. Tidigare forskning saknar i stor utsträckning en systematisk behandling av partiell inverterbarhet, och kopplingen till lokal inverterbarhet är ännu inte välförstådd. I denna avhandling visar vi att med rätt designavvägning kan partiell inverterbarhet uttryckas ovanpå en lokalt inverterbar grund. Vi presenterar KALPIS, ett nytt funktionellt språk som stöder uttrycksfull partiell inverterbarhet, samtidigt som det bibehåller en enkel lokalt inverterbar semantik. Detta formaliseras genom ett nytt Arrow-kombinatorspråk RRARR, vars primitiver representerar funktioner, parameteriserade bijektioner och interaktioner mellan de två. Formuleringen baseras på ny forskning om sidoeffekter i inverterbar beräkning, nämligen irreversibilitetseffekten och reversible reader. Vi substantierar arbetet med en prototypimplementation av KALPIS och visar dess användbarhet genom ett antal icketriviala exempel. Dessutom ger vi en komplett formalisering av de två systemen, inklusive operativ semantik och typsystem för KALPIS och en lokalt inverterbar tolkning och ekvationskaraktärisering av RRARR. Slutligen ger vi en kompositionell översättning från KALPIS till RRARR, vilket motiverar oss att kalla det ett Arrow-metaspråk. Det mesta av formaliseringen är mekaniserad med hjälp av bevisassistenten Agda.

<p align="justify">Une approche multidimensionelle pour la résolution numérique des équations d'Euler et de Navier-Stokes sur maillages non-structurés est proposée. Dans une première partie, un exposé complet des schémas de distribution, dits de "fluctuation-splitting" ,est décrit, comprenant une étude comparative des schémas décentrés, positifs et de 2ème ordre, pour résoudre l'équation de convection à coefficients constants, ainsi qu'une étude théorique et numérique de la précision des schémas sur maillages réguliers et distordus. L'extension à des lois de conservation non-linéaires est aussi abordée, et une attention particulière est portée au problème de la linéarisation conservative. Dans une deuxième partie, diverses discrétisations des termes visqueux pour l'équation de convection-diffusion sont développées, avec pour but de déterminer l'approche qui offre le meilleur compromis entre précision et coût. L'extension de la méthode aux systèmes des lois de conservation, et en particulier à celui des équations d'Euler de la dynamique des gaz, représente le noyau principal de la thèse, et est abordée dans la troisième partie. Contrairement aux schémas de distribution classiques, qui reposent sur une extension formelle du cas scalaire, l'approche développée ici repose sur une décomposition du résidu par élément en équations scalaires, modélisant le transport de variables caracteristiques. La difficulté vient du fait que les équations d'Euler instationnaires ne se diagonalisent pas, et admettent une infinité de solutions élémentaires (ondes simples) se propageant dans toutes les directions d'espace. En régime stationnaire, en revanche, les équations se diagonalisent complètement dans le cas des écoulements supersoniques, et partiellement dans le cas des écoulements subsoniques. Ainsi, les équations sous forme conservative peuvent être remplacées par un système équivalent comprenant deux équations totalement découplées, exprimant l'invariance de l'entropie et de l'enthalpie totale le long des lignes de courant, et deux autres équations, modélisant les effets purement acoustiques. En régime supersonique, celles-ci se découplent aussi, et expriment la convection le long des lignes de Mach d'invariants de Riemann généralisés. La discrétisation de ces équations par des schémas scalaires décentrés permet de simuler des écoulements continus et discontinus avec une grande précision et sans oscillations. Finalement, dans une dernière partie, l'extension aux équations de Navier-Stokes est abordée, et la discrétisation des termes visqueux par une approche éléments finis est proposée. Les résultats numériques confirment la précision et la robustesse de la méthode.</p>

This essay discusses the width of the late medieval desertion of farms in Sweden from an archaeological perspective. The object of the essay is to investigate if archaeological investigations and research during the last 10-15 years have changed the view of the late medieval desertion in relation to the Scandinavian research project on deserted farms and villages. The essay also deals with questions on causes to the desertion and when desertion occurred. An ambition of the essay is also to give a general picture of archaeological investigations during the last 10-15 years considering the late medieval desertion. The analyses-material consists mainly of reports from archaeological investigations. Most of the investigations analysed in this essay are investigations of single farms. Because of this it is natural these investigations do not say much about the width of the desertion. As long as an archaeological investigation is not a part of a large project, where the purpose is to show the width of the desertion, one cannot expect that one single investigation will give much information or knowledge about the width. However, if the ambition is to obtain a complete picture of a medieval deserted farm or village, this essay confirms that an archaeological investigation is necessary, willingly in an interdisciplinary cooperation.

Uppsatsen undersöker hur de upplevda riskerna påverkar stockholmarnas vardagliga liv. Denna studie genomfördes med hjälp av kvalitativ metod och ett induktivt tillvägagångssätt valdes av författaren. 24 intervjuer med stockholmare genomfördes inom ramen för projekten. Dessa, med hjälp av innehållsanalysen bearbetade intervjuer, lades till grund för de slutsatser som presenteras i studien. Uppsatsen uppmärksammar kluvenheten i frågan om uppfattning av sin livsmiljö och dess säkerhet/trygghet som präglar stockholmarnas existens. Den kluvna uppfattningen av säkerhet och trygghet benämns av författaren för den partiella tryggheten. Samexistensen av känslan av trygghet och otrygghet kännetecknar den partiella tryggheten. Upplevelsen av den partiella tryggheten ses i ett större sammanhang och det påvisas hur den vid applicering på stockholmarnas vardag försämrar deras livskvalité, sätter begränsningar på deras rörelse- och handlingsfrihet samt i slutändan gör staden mindre tillgänglig. / The thesis studies how perceived risks affect the daily life of inhabitants of Stockholm, Sweden. The study was conducted through qualitative method and an inductive approach was selected by the author. 24 interviews with Stockholmers were conducted within the framework of the projects. These through the means of content analysis processed interviews were used as a basis for the conclusions presented in the study. The thesis considers the ambiguity in the question of perception of environment and the security/safety thereof, which characterises the existence of Stockholmers. The ambiguous perception of security and safety is by the author named partial safety. Coexistence of the sense of safety and unsafety characterizes partial security. The experience of partial safety is seen as a more comprehensive context and it is shown how it, when applied to the everyday life of Stockholmers, has a negative impact on their quality of life, imposes limits on their freedom of movement and -action, as well as ultimately makes the city less accessible.