Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Teaching mathematics and programming : new approaches with empirical evaluation

Programming and mathematics are core areas of computer science (CS) and consequently also important parts of CS education. Introductory instruction in these two topics is, however, not without problems. Studies show that CS students find programming difficult to learn and that teaching mathematical topics to CS novices is challenging. One reason for the latter is the disconnection between mathematics and programming found in many CS curricula, which results in students not seeing the relevance of the subject for their studies. In addition, reports indicate that students' mathematical capability and maturity levels are dropping. The challenges faced when teaching mathematics and programming at CS departments can also be traced back to gaps in students' prior education. In Finland the high school curriculum does not include CS as a subject; instead, focus is on learning to use the computer and its applications as tools. Similarly, many of the mathematics courses emphasize application of formulas, while logic, formalisms and proofs, which are important in CS, are avoided. Consequently, high school graduates are not well prepared for studies in CS. Motivated by these challenges, the goal of the present work is to describe new approaches to teaching mathematics and programming aimed at addressing these issues: Structured derivations is a logic-based approach to teaching mathematics, where formalisms and justifications are made explicit. The aim is to help students become better at communicating their reasoning using mathematical language and logical notation at the same time as they become more confident with formalisms. The Python programming language was originally designed with education in mind, and has a simple syntax compared to many other popular languages. The aim of using it in instruction is to address algorithms and their implementation in a way that allows focus to be put on learning algorithmic thinking and programming instead of on learning a complex syntax. Invariant based programming is a diagrammatic approach to developing programs that are correct by construction. The approach is based on elementary propositional and predicate logic, and makes explicit the underlying mathematical foundations of programming. The aim is also to show how mathematics in general, and logic in particular, can be used to create better programs.

On the potential utilisation of sawdust and wood chip screenings

This work is based on the utilisation of sawdust and wood chip screenings for different purposes. A substantial amount of these byproducts are readily available in the Finnish forest industry. A black liquor impregnation study showed that sawdust-like wood material behaves differently from normal chips. Furthermore, the fractionation and removal of the smallest size fractions did not have a significant effect on the impregnation of sawdust-like wood material. Sawdust kraft cooking equipped with an impregnation stage increases the cooking yield and decreases the lignin content of the produced pulp. Impregnation also increases viscosity of the pulp and decreases chlorine dioxide consumption in bleaching. In addition, impregnation increases certain pulp properties after refining. Hydrotropic extraction showed that more lignin can be extracted from hardwood than softwood. However, the particle size had a major influence on the lignin extraction. It was possible to extract more lignin from spruce sawdust than spruce chips. Wood chip screenings are usually combusted to generate energy. They can also be used in the production of kraft pulp, ethanol and chemicals. It is not economical to produce ethanol from wood chip screenings because of the expensive wood material. Instead, they should be used for production of steam and energy, kraft pulp and higher value added chemicals. Bleached sawdust kraft pulp can be used to replace softwood kraft pulp in mechanical pulp based papers because it can improve certain physical properties. It is economically more feasible to use bleached sawdust kraft pulp in stead of softwood kraft pulp, especially when the reinforcement power requirement is moderate.

Influence of plasma modification on surface properties and offset printability of coated paper

The properties of the paper surface play a crucial role in ensuring suitable quality and runnability in various converting and finishing operations, such as printing. Plasma surface modification makes it possible to modify the surface chemistry of paper without altering the bulk material properties. This also makes it possible to investigate the role of the surface chemistry alone on printability without influencing the porous structure of the pigment-coated paper. Since the porous structure of a pigment coating controls both ink setting and optical properties, surface chemical changes created by a plasma modification have a potential to decouple these two effects and to permit a better optimization of them both. The aim of this work was to understand the effects of plasma surface modification on paper properties, and how it influences printability in the sheet-fed offset process. The objective was to broaden the fundamental understanding of the role of surface chemistry on offset printing. The effects of changing the hydrophilicity/ hydrophobicity and the surface chemical composition by plasma activation and plasma coatings on the properties of coated paper and on ink-paper interactions as well as on sheet-fed offset print quality were investigated. In addition, the durability of the plasma surface modification was studied. Nowadays, a typical sheet-fed offset press also contains units for surface finishing, for example UVvarnishing. The role of the surface chemistry on the UV-varnish absorption into highly permeable and porous pigment-coated paper was also investigated. With plasma activation it was possible to increase the surface energy and hydrophilicity of paper. Both polar and dispersion interactions were found to increase, although the change was greater in the polar interactions due to induced oxygen molecular groups. The results indicated that plasma activation takes place particularly in high molecular weight components such as the dispersion chemicals used to stabilize the pigment and latex particles. Surface composition, such as pigment and binder type, was found to influence the response to the plasma activation. The general trend was that pilot-scale treatment modified the surface chemistry without altering the physical coating structure, whereas excessive laboratory-scale treatment increased the surface roughness and reduced the surface strength, which led to micro-picking in printing. It was shown that pilot-scale plasma activation in combination with appropriate ink oils makes it possible to adjust the ink-setting rate. The ink-setting rate decreased with linseed-oil-based inks, probably due to increased acid-base interactions between the polar groups in the oil and the plasma-treated paper surface. With mineral-oil-based inks, the ink setting accelerated due to plasma activation. Hydrophobic plasma coatings were able to reduce or even prevent the absorption of dampening water into pigmentcoated paper, even when the dampening water was applied under the influence of nip pressure. A uniform hydrophobic plasma coating with sufficient chemical affinity with ink gave an improved print quality in terms of higher print density and lower print mottle. It was also shown that a fluorocarbon plasma coating reduced the free wetting of the UV-varnish into the highly permeable and porous pigment coating. However, when the UV-varnish was applied under the influence of nip pressure, which leads to forced wetting, the role of the surface chemical composition seems to be much less. A decay in surface energy and wettability occurred during the first weeks of storage after plasma activation, after which it leveled off. However, the oxygen/carbon elemental ratio did not decrease as a function of time, indicating that ageing could be caused by a re-orientation of polar groups or by a contamination of the surface. The plasma coatings appeared to be more stable when the hydrophobicity was higher, probably due to fewer interactions with oxygen and water vapor in the air.

Microscopic simulation of pigment coating consolidation

The control of coating layer properties is becoming increasingly important as a result of an emerging demand for novel coated paper-based products and an increasing popularity of new coating application methods. The governing mechanisms of microstructure formation dynamics during consolidation and drying are nevertheless, still poorly understood. Some of the difficulties encountered by experimental methods can be overcome by the utilisation of numerical modelling and simulation-based studies of the consolidation process. The objective of this study was to improve the fundamental understanding of pigment coating consolidation and structure formation mechanisms taking place on the microscopic level. Furthermore, it is aimed to relate the impact of process and suspension properties to the microstructure of the coating layer. A mathematical model based on a modified Stokesian dynamics particle simulation technique was developed and applied in several studies of consolidation-related phenomena. The model includes particle-particle and particle-boundary hydrodynamics, colloidal interactions, Born repulsion, and a steric repulsion model. The Brownian motion and a free surface model were incorporated to enable the specific investigation of consolidation and drying. Filter cake stability was simulated in various particle systems, and subjected to a range of base substrate absorption rates and system temperatures. The stability of the filter cake was primarily affected by the absorption rate and size of particles. Temperature was also shown to have an influence. The consolidation of polydisperse systems, with varying wet coating thicknesses, was studied using imposed pilot trial and model-based drying conditions. The results show that drying methods have a clear influence on the microstructure development, on small particle distributions in the coating layer and also on the mobility of particles during consolidation. It is concluded that colloidal properties can significantly impact coating layer shrinkage as well as the internal solids concentration profile. Visualisations of particle system development in time and comparison of systems at different conditions are useful in illustrating coating layer structure formation mechanisms. The results aid in understanding the underlying mechanisms of pigment coating layer consolidation. Guidance is given regarding the relationship between coating process conditions and internal coating slurry properties and their effects on the microstructure of the coating.

Reactive dissolution of sedimentary rocks in flue gas desulfurization : modeling and experimental investigation

Svavel förekommer i kol och olja och oxideras vid förbränning till svaveldioxid (SO2). Årligen utsläpps stora mängder svaveldioxid som åstadkommer sura regn, minskning av stratosfäriskt ozon och sjukdomar. Av dessa orsaker är det nödvändigt att minska utsläppen av svaveldioxid. Den teknologi som rör planering av reaktorer och processer för rökgasavsvavling (FGD) har utvecklats kraftigt och idag använder man olika typer av lösningar. De vanligaste alternativen för FGD är våtskrubber- och semitorra skrubbersystem (Spray Dry Scrubbers, SDS) och injektionsprocesser för absorbenter. SDS-processer har studerats bland annat av Ahlbeck [4] och Klingspor [5] och injektionsprocesser av Alvfors [6]. Kalksten, som i huvusak består av kalciumkarbonat, används i rökgasavsvavling på grund av sin förmåga att binda svavel i form av sulfatsalter. Den vanligaste rökgasavsvavlingsmetoden är våtskrubbning, där det sedimentära stenmaterialets upplösningshastighet är en av de faktorer som påverkar resultatet mest. Utvärdering av kalkstensreaktivitet är därför speciellt viktig vid planering och drift av anläggningar för rökgasavsvavling. Målsättningen med detta arbete var att modellera upplösningen av olika typers kalksten för att få en kvantitativ utvärdering av kvaliteten på de analyserade proverna. Därtill testades även karbonatbiprodukter från stålindustrin för att utvärdera möjligheter att använda andra råmaterial. Det transienta förloppet har analyserats, varvid upplösningshastigheten modellerades bl.a. i avseende på tid och pH. Under arbetets gång har antalet empiriska korrelationer minskats till fördel för fysikaliska modeller av diffusiva och konvektiva masstransportfenomen. En målsättning var att skapa en effektiv och snabb metod för att testa olika absorbenter för rökgasavsvavling under transienta förlopp. I arbetet användes PSD-analys, gjordes pH-mätningar och andra utvärderingar av de fysikaliska parametrar som ingår i beräkningarna. On-line mätningar för de icke-stationära variablerna tid och pH ger möjlighet att eliminera osäkerheter. Vissa modeller kan vara komplicerade. En modell för upplösningshastigheten med mer detaljerad utvärdering av parametrar och färre approximationer är därför nödvändig då man vill utvärdera reaktionshastigheten för fasta partiklar i sur miljö. Arbetet utfördes under fyra år och fem peer review-artiklar ingår i avhandlingen.

Boundary identification in the domain of a parabolic partial differential equation

Bakgrunden och inspirationen till föreliggande studie är tidigare forskning i tillämpningar på randidentifiering i metallindustrin. Effektiv randidentifiering möjliggör mindre säkerhetsmarginaler och längre serviceintervall för apparaturen i industriella högtemperaturprocesser, utan ökad risk för materielhaverier. I idealfallet vore en metod för randidentifiering baserad på uppföljning av någon indirekt variabel som kan mätas rutinmässigt eller till en ringa kostnad. En dylik variabel för smältugnar är temperaturen i olika positioner i väggen. Denna kan utnyttjas som insignal till en randidentifieringsmetod för att övervaka ugnens väggtjocklek. Vi ger en bakgrund och motivering till valet av den geometriskt endimensionella dynamiska modellen för randidentifiering, som diskuteras i arbetets senare del, framom en flerdimensionell geometrisk beskrivning. I de aktuella industriella tillämpningarna är dynamiken samt fördelarna med en enkel modellstruktur viktigare än exakt geometrisk beskrivning. Lösningsmetoder för den s.k. sidledes värmeledningsekvationen har många saker gemensamt med randidentifiering. Därför studerar vi egenskaper hos lösningarna till denna ekvation, inverkan av mätfel och något som brukar kallas förorening av mätbrus, regularisering och allmännare följder av icke-välställdheten hos sidledes värmeledningsekvationen. Vi studerar en uppsättning av tre olika metoder för randidentifiering, av vilka de två första är utvecklade från en strikt matematisk och den tredje från en mera tillämpad utgångspunkt. Metoderna har olika egenskaper med specifika fördelar och nackdelar. De rent matematiskt baserade metoderna karakteriseras av god noggrannhet och låg numerisk kostnad, dock till priset av låg flexibilitet i formuleringen av den modellbeskrivande partiella differentialekvationen. Den tredje, mera tillämpade, metoden kännetecknas av en sämre noggrannhet förorsakad av en högre grad av icke-välställdhet hos den mera flexibla modellen. För denna gjordes även en ansats till feluppskattning, som senare kunde observeras överensstämma med praktiska beräkningar med metoden. Studien kan anses vara en god startpunkt och matematisk bas för utveckling av industriella tillämpningar av randidentifiering, speciellt mot hantering av olinjära och diskontinuerliga materialegenskaper och plötsliga förändringar orsakade av “nedfallande” väggmaterial. Med de behandlade metoderna förefaller det möjligt att uppnå en robust, snabb och tillräckligt noggrann metod av begränsad komplexitet för randidentifiering.

Crystallization characteristics of bioactive glasses

Bioactive glasses are excellent candidates for implant materials, because they can form a chemical bond to bone or guide bone growth, depending on the glass composition. Some compositions have even shown soft tissue attachment and antimicrobial effects. So far, most clinical applications are based on monoliths, plates and particulates of different grain sizes. There is a growing interest in special products such as porous implants sintered from microspheres and fibers drawn from preforms or glass melts. The viscosity range at which these are formed coincides with the crystallization temperature range for most bioactive glasses, thus complicating the manufacturing process. In this work, the crystallization tendency and its kinetics for a series of glasses with their compositions within the range of bioactivity were investigated. The factors affecting crystallization and how it is related to composition were studied by means of thermal analysis and hot stage microscopy. The crystal compositions formed during isothermal and non-isothermal heat treatments were analyzed with SEM-EDXA and X-ray diffraction analysis. The temperatures at which sintering and fiber drawing can take place without interfering with crystallization were determined and glass compositions which are suitable for these purposes were established. The bioactivity of glass fibers and partly crystallized glass plates was studied by soaking them in simulated body fluid (SBF). The thickness of silica, calcium and phosphate rich reaction layers on the glass surface after soaking was used as an indication of the bioactivity. The results indicated that the crystallization tendencies of the experimental glasses are strongly dependent on composition. The main factor affecting the crystallization was found to be the alkali oxide content: the higher the alkali oxide content the lower the crystallization temperature. The primary crystalline phase formed at low temperatures in these glasses was sodium calcium silicate. The crystals were found to form through internal nucleation, leading to bulk crystallization. These glasses had high bioactivity in vitro. Even when partially crystalline, they formed typical reaction layers, indicating bioactivity. In fact, sodium calcium silicate crystals were shown to transform in vitro into hydroxyapatite during soaking. However, crystallization should be avoided because it was shown to retard dissolution, bioactivity reactions and complicate fiber drawing process. Glass compositions having low alkali oxide content showed formation of wollastonite crystals on the surface, at about 300°C above the glass transition temperature. The wide range between glass transition and crystallization allowed viscous flow sintering of these compositions. These glasses also withstood the thermal treatments required for fiber drawing processing. Precipitation of calcium and phosphate on fibers of these glasses in SBF suggested that they were osteoconductive. Glasses showing bioactivity crystallize easily, making their hot working challenging. Undesired crystallization can be avoided by choosing suitable compositions and heat treatment parameters, allowing desired product forms to be attained. Small changes in the oxide composition of the glass can have large effects and therefore a thorough understanding of glass crystallization behavior is a necessity for a successful outcome, when designing and manufacturing implants containing bioactive glasses.

Distribution and role of macrophytes in coastal lagoons : implications of critical shifts

Crossroads, crucibles and refuges are three words that may describe natural coastal lagoon environments. The words refer to the complex mix of marine and terrestrial influences, prolonged dilution due to the semi-enclosed nature and the function of a habitat for highly diverse plant and animal communities, some of which are endangered. To attain a realistic picture of the present situation, high vulnerability to anthropogenic impact should be added to the description. As the sea floor in coastal lagoons is usually entirely photic, macrophyte primary production is accentuated compared with open sea environments. There is, however, a lack of proper knowledge on the importance of vegetation for the general functioning of coastal lagoon ecosystems. The aim of this thesis is to assess the role of macrophyte diversity, cover and species identity over temporal and spatial scales for lagoon functions, and to determine which steering factors primarily restrict the qualitative and quantitative composition of vegetation in coastal lagoons. The results are linked to patterns of related trophic levels and the indicative potential of vegetation for assessment of general conditions in coastal lagoons is evaluated. This thesis includes five field studies conducted in flads and glo-flads in the brackish water northern Baltic Sea. Flads and glo-flads are defined as a Baltic variety of coastal lagoons, which due to an inlet threshold and post-glacial landuplift slowly will be isolated from the open sea. This process shrinks inlet size, increases exposure and water retention, and is called habitat isolation. The studied coastal lagoons are situated in the archipelago areas of the eastern coast of Sweden, the Åland Islands and the south-west mainland of Finland, where land-uplift amounts to ca. 5 mm/ per year. Out of 400 evaluated sites, a total of 70 lagoons varying in inlet size, archipelago position and anthropogenic influence to cover for essential environmental variation were chosen for further inventory. Vegetation composition, cover and richness were measured together with several hydrographic and morphometric variables in the lagoons both seasonally and inter-annually to cover for general regional, local and temporal patterns influencing lagoon and vegetation development. On smaller species-level scale, the effects of macrophyte species identity and richness for the fish habitat function were studied by examining the influence of plant interaction on juvenile fish diversity. Thus, the active election of plant monoand polycultures by fish and the diversity of fish in the respective culture were examined and related to plant height and water depth. The lagoons and vegetation composition were found to experience a regime shift initiated by increased habitat isolation along with land-uplift. Vegetation composition altered, richness decreased and cover increased forming a less isolated and more isolated regime, named the vascular plant regime and charophyte regime, respectively according to the dominant vegetation. As total phosphorus in the water, turbidity and the impact of regional influences decreased in parallel, the dominance of charophytes and increasing cover seemed to buffer and stabilize conditions in the charophyte regime and indicated an increased functional role of vegetation for the lagoon ecosystem. The regime pattern was unaffected by geographical differences, while strong anthropogenic impact seemed to distort the pattern due to loss of especially Chara tomentosa L. in the charophyte regime. The regimes were further found unperturbed by short-time temporal fluctuations. In fact the seasonal and inter-annual dynamics reinforced the functional difference between the regimes by the increasing role of vegetation along habitat isolation and the resemblance to lake environments for the charophyte regime. For instance, greater total phosphorus and chlorophyll a concentrations in the water in the beginning of the season in the charophyte regime compared with the vascular plant regime presented a steeper reduction to even lower values than in the vascular plant regime along the season. Despite a regional importance and positive relationship of macrophyte diversity in relation to trophic diversity, species identity was underlined in the results of this thesis, especially with decreasing spatial scale. This result was supported partly by the increased role of charophytes in the functioning of the charophyte regime, but even more explicitly by the species-specific preference of juvenile fish for tall macrophyte monocultures. On a smaller species-level scale, tall plant species in monoculture seemed to be able to increase their length, indicating that negative selection forms preferred habitat structures, which increase fish diversity. This negative relationship between plant and fish diversity suggest a shift in diversity patterns among trohic levels on smaller scale. Thus, as diversity patterns seem complex and diverge among spatial scales, it might be ambiguous to extend the understanding of diversity relationships from one trophic level to the other. All together, the regime shift described here presents similarities to the regime development in marine lagoon environments and shallow lakes subjected to nutrient enrichment. However, due to nutrient buffering by vegetation with increased isolation and water retention as a consequence of the inlet threshold, the development seems opposite to the course along an eutrophication gradient described in marine lagoons lacking an inlet threshold, where the role of vegetation decreases. Thus, the results imply devastating consequences of inlet dredging (decreasing isolation) in terms of vegetation loss and nutrient release, and call for increased conservational supervision. Especially the red listed charophytes would suffer negatively from such interference and the consequences are likely to also deteriorate juvenile fish production. The fact that a new species to Finland, Chara connivens Salzm. Ex. Braun 1835 was discovered during this study further indicates a potential of the lagoons serving as refuges for rare species.

Mantle- and crust-derived magmatism in the southern Fennoscandian Shield at c. 1.8 Ga; evidence from geochemistry, isotopes and geochronology

Geokemi och isotopsammansättningarna hos ca 1,8 Ga (miljarder år) gamla mafiska bergartsintrusioner studerades i två huvudområden: i) Transskandinaviska magmatiska bältet (TMB) i Bergslagen, Småland och Blekinge, södra Sverige, inklusive några prov från det ca 1,87 Ga gamla Hedesunda-komplexet i östra Bergslagen, samt ii) mindre, postkollisionala komplex i södra Finland och ryska Karelen. I det senare fallet var även tillhörande granitoider inkluderade i studierna. TMB-bergarterna skiljer sig avsevärt i utvecklingsgrad och omfattar sammansättningsmässigt bergarter från ultramafiter till kvartsdioriter. Dessa bergarters geokemi är kännetecknande för kontinentala öbågar. För sydligaste TMB och Hedesunda antyder geokemin en något mera oceanisk öbågekaraktär. Tillsammans med tidigare data antyder de av Rutanen analyserade Nd- och Sr-isotopförhållanden för TMB en ’milt utarmad’ mantelsammansättning. De mafiska bergarterna i södra Finland och ryska Karelen varierar från ultramafiska till monzodioritiska, men med avsevärt högre alkalihalter jämfört med TMB. Källan för all den studerade mafiska magmatismen kan beskrivas som en utarmad mantel som i varierande grad påverkats av fluider och smältor ur subducerande litosfärplattor. Geokemin antyder infiltrering och påverkning av H2O-dominerande fluider i övre manteln för TMB. Den mafiska ca 1,8 Ga gamla magmatismen österut avspeglar en ökande påverkan av sedimentderiverade karbonatfluider och smältor inom allt djupare mantelområden. Denna subduktionsrelaterade mantelanrikning skedde under den föregående öbågeutvecklingen i södra delarna av Finland och Sverige, samt ryska Karelen. Geokemin för en grupp granitoider, associerade med de ca 1,8 Ga gamla intrusionerna i södra Finland visar både vulkanisk öbåge och synkollisional granitoidkaraktär. Denna grupp har ett blandat magmatiskt och sedimentärt Svekofenniskt ursprung, vilket kan antas p.g.a. deras Nd- och Sr-isotopförhållanden. En annan grupp av granitoider ligger geokemiskt mellan vulkanisk öbåge- och intraplatt-granitoider, och har magmatiskt ursprung. Geokemin och isotoperna hos dessa intrusioner kan förklaras med hybridisering mellan de kraftigt anrikade, mantelderiverade magmorna, och granitmagmor från den äldre skorpan. Den ca 1,8 Ga gamla TMB-magmatismen i Sverige skedde vid sammanslutning av kontinentalrandbågar, med kontinuerlig subduktion mot öster i Bergslagen, och mot norr i de sydligare delarna. Samtidigt i öster intruderade de postkollisionala intrusionerna i skorpan omedelbart efter kollisionen med den Volgo-Sarmatiska kontinenten från sydost. Denna invecklade paleotektoniska konfiguration orsakade en tektonisk regim där litosfäriska mantelkällor levererade de starkt anrikade magmorna, vilkas uppstigning troligen möjliggjordes av djupgående postkollisionala skjuvzoner. Intrusionerna orsakade uppsmältning av den omgivande skorpan, vilket framkallade den associerade granitoidmagmatismen.

Ion modulated organic transistors

I likhet med vanliga plaster är de π-konjugerade polymererna flexibla, lösliga och processbara vid låga temperaturer (< 150 ºC). Därutöver har de egenskapen att leda ström. Konduktivitetsintervallet är brett och omfattar nästintill metallisk ledningsförmåga å ena sidan, via halvledarkonduktiva till isolerande å andra sidan. Polymererna utgörs av regelbundna kedjor av kolatomer och associeras sålunda till organiska material. Sedan de första vetenskapliga rapporterna publicerades vid slutet av 1970-talet har π-konjugerade polymerer använts och utvecklats i exempelvis solceller, dioder, lysdioder och transistorer. Nobelpriset i kemi tilldelades år 2000 åt Hideki Shirakawa, Alan J. Heeger och Alan G. MacDiarmid för upptäckten och utvecklandet av ledande polymerer. I min avhandling har jag arbetat med att utveckla och förstå lågspännings jonmodulerade organiska transistorer. Två typer av jonmodulerade organiska transistorer studeras: (1) den jonmodulerade organiska fälteffekt transistorn (jonmodulerade OFETen), som utgör den centrala transistorn i avhandlingen, samt (2) den elektrokemiska transistorn. Den första typen fungerar som en konventionell OFET. Strömmen i halvledaren moduleras av det elektriska fältet över isolatorn. Med användandet av en elektrolyt ”isolator” orsakar polariseringen av jonerna däremot ett högt elektriskt fält vid elektrolyt/halvledargränssnittet och man åstadkommer modulering av strömmen redan vid några volts drivspänningar. I den andra typen utnyttjas elektrokemi för att medelst reduktion/oxidation modulera strömmen i den π-konjugerade polymeren. Ett viktigt ändamål i avhandlingen har också varit att kunna tillverka transistorerna med masstillverkningsmetoder. I avhandlingen presenteras de jonmodulerade organiska transistorernas möjlighet att framställas med masstillverkningsmetoder. Nya koncept introduceras och svagheter identifieras. Skillnaderna mellan OFETen, jonmodulerade OFETen och den elektrokemiska transistorn klargörs. Arbetet skall däremot inte anses fullbordat utan forskningen fortgår för att kringgå svagheterna, öka på transistorernas stabilitet och framförallt tillämpa dem i innovativa applikationer.

Influence of topography and surface chemistry on the wetting properties of TiO2-based ceramic coatings

Vätning av fasta ytor är ett viktigt fenomen i såväl naturen som i en lång rad av industriella tillämpningar. Det är allmänt känt att vätningen av en fast yta styrs av ytans kemi samt struktur. Målsättningen med avhandlingen var att studera hur kemisk heterogenitet och ytråhet på nanometernivå påverkar vätningsegenskaperna hos en fast yta. Ytorna som studerades var titandioxid-baserade kerama ytor som framställdes med hjälp av en sol-gel process. Vätningstudierna utfördes genom kontaktvinkelmätningar, vilket innebär att man mäter vinkeln som vätska/luft-gränsskiktet hos en vätskedroppe bildar mot en fast yta. Ytråheten hos materialen studerades främst genom atomkraftsmikroskopi (AFM). I AFM detekteras ytans struktur av en mycket skarp nål som skannar ytan. Resultaten i avhandlingen kunde framgångsrikt modelleras med existerande teorier för vätning av heterogena ytor.

Some defects in two-dimensional spin-1/2 Heisenberg antiferromagnets: a numerical study of magnetic effects

En del av de intressantaste fenomenen inom dagens materialfysik uppstår ur ett intrikat samspel mellan myriader av elektroner. Högtemperatursupraledare är det mest berömda exemplet. Varken klassiska teorier eller modeller där elektronerna är oberoende av varandra kan förklara de häpnadsväckande effekterna i de starkt korrelerade elektronsystemen. I vissa kopparoxider, till exempel La2CuO4, är det känt att valenselektronerna till följd av en stark ömsesidig växelverkan lokaliseras en och en till kopparatomerna i föreningens CuO2 plan. Laddningarnas inneboende magnetiska moment—spinnet—får då en avgörande roll för materialets elektriska och magnetiska egenskaper, vilka i exemplets fall kan beskrivas med Heisenbergmodellen som är den grundläggande teoretiska modellen för mikroskopisk magnetism. Men exakt varför föreningarna kan bli supraledande då de dopas med överskottsladdningar är än så länge en obesvarad fråga. Min avhandling undersöker orenheters inverkan på Heisenbergmodellens magnetiska egenskaper—ett problem av både experimentell och teoretisk relevans. En etablerad numerisk metod har använts—en kvantmekanisk Monte Carlo teknik—för att utföra omfattande datorsimuleringar av den matematiska modellen på två dedikerade Linux datorkluster. Arbetet hör till området beräkningsfysik. De teoretiska modellerna för starkt korrelerade elektronsystem, däribland Heisenbergmodellen, är ytterst invecklade matematiskt sett och de kan inte lösas exakt. Analytiska utredningar bygger för det mesta på antaganden och förenklingar vars inverkningar på slutresultatet är ofta oklara. I det avseende kan numeriska studier vara exakta, det vill säga de kan behandla modellerna som de är. Oftast behövs bägge tillvägagångssätten. Den röda tråden i arbetet har varit att numeriskt testa vissa högaktuella analytiska förutsägelser rörande effekterna av orenheter i Heisenbergmodellen. En del av dem har vi på basen av mycket noggranna data kunnat bekräfta. Men våra resultat har också påvisat felaktigheter i de analytiska prognoserna som sedermera delvis reviderats. En del av avhandlingens numeriska upptäckter har i sin tur stimulerat till helt nya teoretiska studier.

Dynamic interplay between the intermediate filament protein nestin and Cyclin-dependent kinase 5

Cellen har ett s.k. cytoskelett som bl.a. ger stadga åt cellen och deltar i dess form- och rörelsefunktioner. Intermediärfilamenten är en viktig del av cytoskelettet och de har länge varit kända för sina väsentliga roller i att upprätthålla den cellulära organisationen och vävnadernas integritet. På senare år har man insett att intermediärfilamenten har en större funktionell mångsidighet än man tidigare tänkts sig, i och med att en rad olika studier har visat betydelsen av intermediärfilamenten vid olika signaleringprocesser. Dessa proteinnätverk samverkar nämligen med kinaser och andra viktiga signalfaktorer och deltar därmed i cellens signaleringmaskineri. Intermediärfilamentproteinet nestin används ofta som en markör för stamceller men dess fysiologiska funktioner är i stort sett okända. Interaktion mellan nestin och ett signalkomplex bestående av cyklin-beroende kinas 5 (eng. Cyclin-dependent kinase, Cdk5) och dess aktivatorprotein p35 upptäcktes i vårt laboratorium före denna avhandling påbörjades. Därför var syftet med min avhandling att undersöka den funktionella betydelsen av nestin i regleringen av Cdk5/p35 komplexet. Cdk5 är ett multifunktionellt kinas som reglerar både utvecklingen och stressreaktioner i nerver och muskler. Vi visade att nestin skyddar neuronala stamceller under oxidativ stress genom dess förmåga att hämma Cdk5s skadliga aktivitet. Genom att förankra Cdk5/p35 komplexet, reglerar nestin den subcellulära lokaliseringen av Cdk5/p35 och minskar klyvningen av p35 till den mer stabila aktivatorn p25. Vi demonstrerade också aktiveringsmekanismen för Cdk5 under differentiering av muskelceller. Proteinkinas C zeta (PKCzeta) avslöjades ha en förmåga att accelera klyvningen av p35 till p25, och därmed öka aktiviteten hos Cdk5. Nestin kunde genom sin förmåga att reglera Cdk5 signalkomplexet styra muskelcellernas differentiering. Denna doktorsavhandling har på ett avgörande vis ökat förståelsen av de reglerande mekanismer som styr Cdk5 aktivering. Avhandling presenterar nestin och PKCzeta som kritiska faktorer i denna reglering. Vidare innehåller avhandlingen ny information om de cellulära funktionerna hos nestin som vi har visat vara en viktig reglerare av cellernas överlevnad och differentiering.