Dependent types can be used to capture useful properties about programs at compile time. However, developing dependently typed programs can be difficult in current systems. Capturing interesting program properties usually requires the user to write proofs, where constructing the latter can be both a difficult and tedious process. Additionally, finding and fixing errors in program scripts can be challenging. This thesis concerns ways in which functional programming with dependent types can be made easier. In particular, we focus on providing help for developing programs that incorporate user-defined types and user-defined functions. For the purpose of supporting dependently typed programming, we have designed a framework that provides improved proof automation and error feedback. Proof automation is provided with the use of heuristic based tactics that automate common patterns of proofs that arise when programming with dependent types. In particular, we use heuristics for generalising goals and employ the rippling heuristic for guiding inductive and non-inductive proofs. The automation we describe includes features for caching and reusing lemmas proven during proof search and, whenever proof search fails, the user can assist the prover by providing high-level hints. We concentrate on providing improved feedback for the errors that occur when there is a mismatch between the specification of a program, described with the use of dependent types, and the behaviour of the program. We employ a QuickCheck-like testing tool for automatically identifying these forms of errors, where the counter examples generated are used as error messages. To demonstrate the effectiveness of our framework for supporting dependently typed programming, we have developed a prototype based around the Coq theorem prover. We demonstrate that the framework as a whole makes program development easier by conducting a series of case studies. In these case studies, which involved verifying properties of tail recursive functions, sorting functions and a binary adder, a significant number of the proofs required were automated.

Thermcapillary convection has been known as the dominant force in the flow and heat transfer during metals processings such as welding, drilling, cutting, and crystial growth, etc. Convection in the molten metal is typically vigorous and significant to the results of the process, in that it affects the size and shape of the pool, heat transfer, mixing of solutes, and ultimately microstructure of the finished product. In a melting or solidification process, thermocapillary effects may induce variations in local heat transfer, melting or solidification rates at the solid-liquid interface. thermocapillary flow originates at the hot wall and forms a surface layer along the free surface. The surface layer is driven by the thermocapillary force balanced by viscous stress. This region is followed by a region where the thermocapillary driving force has diminished due to a reduced temperature gradient. steady-state convection induced by thermocapillary and buoyant forces near a corner region of an enclosure having an inclined wall is numerically studied.Introducing an immobilizationt transformation, the shapes of the free surface subject to an incident flux are predicted by simultaneously solving mass, momentum and energy equations in the liquid and energy equation in the surrounding solid. The results provide a deep insight into local heat transfer, melting ¡Nsolidification rates at the solid-liquid interface and defects such as rippling, undercutting, humping, porosity, segregation, etc.

No description available.

The present work researches influence of energy focusing effect to the fusion zone defects in the electron beam welding, which include fusion zone shape, welding depth, welding width, rippling and spiking. And to verify the model of welding defects base on theory and experiment. A spike is a sudden increase in penetration beyond what might be called the average penetration line. Many spikes have voids and cold shuts in their lower portions, because molten metal does not fill in completely, producing a condition similar to a cold shut in a casting. Ripples on a workpiece surface are generally associated with segregation, porosity and other microstructure defects. These become the objectives in this project.

No description available.

No description available.

No description available.

Abstract Carbon nanotubes (CNTs) have extraordinary mechanical and electrical properties. Together with their small dimensions and low density, they are attractive candidates for building blocks in future nanoelectromechanical systems and for many other applications. The extraordinary properties are however only attained by perfectly crystalline CNTs and quickly deteriorate when defects are introduced to the structure. The growth technique affects the crystallinity where in general CNTs grown by arc-discharge are close to perfectly crystalline, while CVD-grown CNTs have large defect densities. Mechanical deformation also affects these properties, even without introducing defects. When CNTs are bent they behave similarly to drinking straws, i.e. they buckle or ripple and their bending stiffness drops abruptly. In this thesis, the mechanical behaviour of individual CNTs and vertically aligned carbon nanofibers (VACNFs) has been studied by performing force measurements inside electron microscopes. Cantilevered CNTs, and VACNFs, were bent using a force sensor, yielding force-deflection curves while their structure was imaged simultaneously. We have found that CNTs grown by arc-discharge have a high enough crystallinity to possess a Young’s modulus close to the ideal value of 1 TPa. CVD-grown CNTs possess a Young’s modulus that is about one order of magnitude smaller, due to their large defect density. The VACNFs are yet another order of magnitude softer as a result of their cup-stacked internal structure.  We also found that a high defect density will increase the critical strain for the rippling onset and the relative post-rippling stiffness. Multi-walled CNTs with a small inner diameter are less prone to ripple and have a larger relative post-rippling stiffness. Our findings show large variations in the onset of rippling and the bending stiffness before and after rippling. These variations open up possibilities of tailoring the mechanical properties for specific applications. / Baksidetext Carbon nanotubes (CNTs) have extraordinary mechanical and electrical properties. Together with their small dimensions and low density, they are attractive candidates for building blocks in nanoelectromechanical systems (NEMS), and many other applications.  In this thesis the mechanical behaviour of individual CNTs and vertically aligned carbon nanofibers has been studied by performing force measurements inside electron microscopes. We have found that the mechanical behaviour is very sensitive to the defect density and the internal structure of the CNTs. The extraordinary properties are only attained by defect free CNTs and quickly deteriorate if defects are introduced to the structure. Mechanical deformations also alter these properties. Single-walled CNTs behave similarly to drinking straws when bent, i.e. they buckle, while the inner tubes of multi-walled CNTs prevent buckling. Instead a more distributed rippling pattern is created for multi-walled CNTs. Both these deformation behaviours will cause an abrupt drop in the bending stiffness, which is detrimental for many applications. The findings in this work will have implications for the design of future NEMS. / <p>Artikel 2 Image formation mechanisms tidigare som manuskript, nu publicerad: urn:nbn:se:kau:diva-16425 (MÅ 150924)</p>

Collisionless shocks are widespread phenomena in the universe, and understanding the mechanisms behind their energy dissipation, with a rare number of collisions between particles, remains a significant unresolved question. The Earth’s bow shock provides an excellent opportunity to study this phenomena in situ. For high Mach number shocks, the shock cannot be sustained without partial reflection of the incoming ions. At higher Mach numbers, the shock surface starts to exhibit non-stationary behaviours, meaning that the shock surface starts evolving. One such behaviour is known as shock reformation, where a new shock forms upstream of an existing one. This study aims to investigate shock reformation using data obtained from NASA’s MMS mission, which offers precise measurements with high spatial and temporal resolutions through its constellation of four spacecraft. Using the MMS shocks database (Lalti et al., 2022), the gradient of the magnetic field magnitude is computed to infer non-stationary behaviour and identify potential instances of shock reformation and other shock behaviours. Through the analysis of the MMS measurements, some insight into the non-stationary characteristics of shocks is obtained using the gradient of the magnetic field. However, further analysis is needed in order to refine the method of identifying non-stationary behaviour of shocks, for future applications. / Kollisionsfria chocker är ett vanligt fenomen som förekommer i universum, och att förstå hur energidissipation inträffar i chocker med ett fåtal kollisioner mellan partikar är ett olöst problem. Jordens bogchock utger en bra möjlighet att studera detta på plats med mätningar från rymdfarkoster. Detta projekt försöker studera delar av jordens bogchock och undersöka dess dynamic. För chocker med högt machtal, måste en del av jonerna från solvinden reflekteras för att chocken ska skunna upprätthållas. Vid högre machtal kan chockytan visa icke-stationära beteenden, vilket innebär att den börjar förändras. Ett exempel på sådant beteende är chockreformation, där en ny chock formas framför en befintlig chock. Denna studie har som mål att undersöka chockreformation med hjälp av data som erhållits från NASA:s MMS-uppdrag, vilket erbjuder precisa mätningar med hög rumslig och tidsmässig upplösning genom sin konstellation av fyra rymdfarkoster. Genom användning av MMS-shockdatabasen (Lalti et al., 2022) beräknades gradienten av magnetfältets magnitud för att härleda icke-stationärt beteende och identifierade potentiella fall av chockreformation och andra beteenden. Genom analys av MMS-mätningarna erhölls viss insikt i de icke-stationära egenskaperna hos chocker med hjälp av gradienten av magnetfältet, men ytterligare analys krävs för att förbättra metoden för framtida tillämpningar.