-
Ordinal Exponentiation in Homotopy Type Theory
Authors:
Tom de Jong,
Nicolai Kraus,
Fredrik Nordvall Forsberg,
Chuangjie Xu
Abstract:
We present two seemingly different definitions of constructive ordinal exponentiation, where an ordinal is taken to be a transitive, extensional, and wellfounded order on a set. The first definition is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classica…
▽ More
We present two seemingly different definitions of constructive ordinal exponentiation, where an ordinal is taken to be a transitive, extensional, and wellfounded order on a set. The first definition is abstract, uses suprema of ordinals, and is solely motivated by the expected equations. The second is more concrete, based on decreasing lists, and can be seen as a constructive version of a classical construction by Sierpi{ń}ski based on functions with finite support. We show that our two approaches are equivalent (whenever it makes sense to ask the question), and use this equivalence to prove algebraic laws and decidability properties of the exponential. Our work takes place in the framework of homotopy type theory, and all results are formalized in the proof assistant Agda.
△ Less
Submitted 20 May, 2025; v1 submitted 24 January, 2025;
originally announced January 2025.
-
From Code to Compliance: Assessing ChatGPT's Utility in Designing an Accessible Webpage -- A Case Study
Authors:
Ammar Ahmed,
Margarida Fresco,
Fredrik Forsberg,
Hallvard Grotli
Abstract:
Web accessibility ensures that individuals with disabilities can access and interact with digital content without barriers, yet a significant majority of most used websites fail to meet accessibility standards. This study evaluates ChatGPT's (GPT-4o) ability to generate and improve web pages in line with Web Content Accessibility Guidelines (WCAG). While ChatGPT can effectively address accessibili…
▽ More
Web accessibility ensures that individuals with disabilities can access and interact with digital content without barriers, yet a significant majority of most used websites fail to meet accessibility standards. This study evaluates ChatGPT's (GPT-4o) ability to generate and improve web pages in line with Web Content Accessibility Guidelines (WCAG). While ChatGPT can effectively address accessibility issues when prompted, its default code often lacks compliance, reflecting limitations in its training data and prevailing inaccessible web practices. Automated and manual testing revealed strengths in resolving simple issues but challenges with complex tasks, requiring human oversight and additional iterations. Unlike prior studies, we incorporate manual evaluation, dynamic elements, and use the visual reasoning capability of ChatGPT along with the prompts to fix accessibility issues. Providing screenshots alongside prompts enhances the LLM's ability to address accessibility issues by allowing it to analyze surrounding components, such as determining appropriate contrast colors. We found that effective prompt engineering, such as providing concise, structured feedback and incorporating visual aids, significantly enhances ChatGPT's performance. These findings highlight the potential and limitations of large language models for accessible web development, offering practical guidance for developers to create more inclusive websites.
△ Less
Submitted 7 January, 2025;
originally announced January 2025.
-
Responsible Composition and Optimization of Integration Processes under Correctness Preserving Guarantees
Authors:
Daniel Ritter,
Fredrik Nordvall Forsberg,
Stefanie Rinderle-Ma
Abstract:
Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scenarios. For integration scenarios, structurally correct composition of patterns into processes and improvements of integration processes are crucial. In order to achieve this, we formalize compositions of integration patte…
▽ More
Enterprise Application Integration deals with the problem of connecting heterogeneous applications, and is the centerpiece of current on-premise, cloud and device integration scenarios. For integration scenarios, structurally correct composition of patterns into processes and improvements of integration processes are crucial. In order to achieve this, we formalize compositions of integration patterns based on their characteristics, and describe optimization strategies that help to reduce the model complexity, and improve the process execution efficiency using design time techniques. Using the formalism of timed DB-nets - a refinement of Petri nets - we model integration logic features such as control- and data flow, transactional data storage, compensation and exception handling, and time aspects that are present in reoccurring solutions as separate integration patterns. We then propose a realization of optimization strategies using graph rewriting, and prove that the optimizations we consider preserve both structural and functional correctness. We evaluate the improvements on a real-world catalog of pattern compositions, containing over 900 integration processes, and illustrate the correctness properties in case studies based on two of these processes.
△ Less
Submitted 17 February, 2024; v1 submitted 30 May, 2023;
originally announced May 2023.
-
Set-Theoretic and Type-Theoretic Ordinals Coincide
Authors:
Tom de Jong,
Nicolai Kraus,
Fredrik Nordvall Forsberg,
Chuangjie Xu
Abstract:
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoret…
▽ More
In constructive set theory, an ordinal is a hereditarily transitive set. In homotopy type theory (HoTT), an ordinal is a type with a transitive, wellfounded, and extensional binary relation. We show that the two definitions are equivalent if we use (the HoTT refinement of) Aczel's interpretation of constructive set theory into type theory. Following this, we generalize the notion of a type-theoretic ordinal to capture all sets in Aczel's interpretation rather than only the ordinals. This leads to a natural class of ordered structures which contains the type-theoretic ordinals and realizes the higher inductive interpretation of set theory. All our results are formalized in Agda.
△ Less
Submitted 12 June, 2023; v1 submitted 25 January, 2023;
originally announced January 2023.
-
Type-Theoretic Approaches to Ordinals
Authors:
Nicolai Kraus,
Fredrik Nordvall Forsberg,
Chuangjie Xu
Abstract:
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection…
▽ More
In a constructive setting, no concrete formulation of ordinal numbers can simultaneously have all the properties one might be interested in; for example, being able to calculate limits of sequences is constructively incompatible with deciding extensional equality. Using homotopy type theory as the foundational setting, we develop an abstract framework for ordinal theory and establish a collection of desirable properties and constructions. We then study and compare three concrete implementations of ordinals in homotopy type theory: first, a notation system based on Cantor normal forms (binary trees); second, a refined version of Brouwer trees (infinitely-branching trees); and third, extensional well-founded orders.
Each of our three formulations has the central properties expected of ordinals, such as being equipped with an extensional and well-founded ordering as well as allowing basic arithmetic operations, but they differ with respect to what they make possible in addition. For example, for finite collections of ordinals, Cantor normal forms have decidable properties, but suprema of infinite collections cannot be computed. In contrast, extensional well-founded orders work well with infinite collections, but almost all properties are undecidable. Brouwer trees take the sweet spot in the middle by combining a restricted form of decidability with the ability to work with infinite increasing sequences.
Our three approaches are connected by canonical order-preserving functions from the "more decidable" to the "less decidable" notions. We have formalised the results on Cantor normal forms and Brouwer trees in cubical Agda, while extensional well-founded orders have been studied and formalised thoroughly by Escardo and his collaborators. Finally, we compare the computational efficiency of our implementations with the results reported by Berger.
△ Less
Submitted 17 May, 2023; v1 submitted 7 August, 2022;
originally announced August 2022.
-
Translating Extensive Form Games to Open Games with Agency
Authors:
Matteo Capucci,
Neil Ghani,
Jérémy Ledent,
Fredrik Nordvall Forsberg
Abstract:
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making prog…
▽ More
We show open games cover extensive form games with both perfect and imperfect information. Doing so forces us to address two current weaknesses in open games: the lack of a notion of player and their agency within open games, and the lack of choice operators. Using the former we construct the latter, and these choice operators subsume previous proposed operators for open games, thereby making progress towards a core, canonical and ergonomic calculus of game operators. Collectively these innovations increase the level of compositionality of open games, and demonstrate their expressiveness.
△ Less
Submitted 3 November, 2022; v1 submitted 14 May, 2021;
originally announced May 2021.
-
Connecting Constructive Notions of Ordinals in Homotopy Type Theory
Authors:
Nicolai Kraus,
Fredrik Nordvall Forsberg,
Chuangjie Xu
Abstract:
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (…
▽ More
In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinals in homotopy type theory, and show how they relate to each other: A notation system based on Cantor normal forms, a refined notion of Brouwer trees (inductively generated by zero, successor and countable limits), and wellfounded extensional orders. For Cantor normal forms, most properties are decidable, whereas for wellfounded extensional transitive orders, most are undecidable. Formulations for Brouwer trees are usually partially decidable. We demonstrate that all three notions have properties expected of ordinals: their order relations, although defined differently in each case, are all extensional and wellfounded, and the usual arithmetic operations can be defined in each case. We connect these notions by constructing structure preserving embeddings of Cantor normal forms into Brouwer trees, and of these in turn into wellfounded extensional orders. We have formalised most of our results in cubical Agda.
△ Less
Submitted 21 July, 2021; v1 submitted 6 April, 2021;
originally announced April 2021.
-
Compositional Game Theory, Compositionally
Authors:
Robert Atkey,
Bruno Gavranović,
Neil Ghani,
Clemens Kupke,
Jérémy Ledent,
Fredrik Nordvall Forsberg
Abstract:
We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new Arrows from old. We model equilibria as a bimodule over an Arrow and define an operator to build a new Arrow from such a bimodule over an existing Arrow. We also model strategies as graded Ar…
▽ More
We present a new compositional approach to compositional game theory (CGT) based upon Arrows, a concept originally from functional programming, closely related to Tambara modules, and operators to build new Arrows from old. We model equilibria as a bimodule over an Arrow and define an operator to build a new Arrow from such a bimodule over an existing Arrow. We also model strategies as graded Arrows and define an operator which builds a new Arrow by taking the colimit of a graded Arrow. A final operator builds a graded Arrow from a graded bimodule. We use this compositional approach to CGT to show how known and previously unknown variants of open games can be proven to form symmetric monoidal categories.
△ Less
Submitted 25 January, 2021;
originally announced January 2021.
-
Compositional Game Theory with Mixed Strategies: Probabilistic Open Games Using a Distributive Law
Authors:
Neil Ghani,
Clemens Kupke,
Alasdair Lambert,
Fredrik Nordvall Forsberg
Abstract:
We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games form a symmetric monoidal category, which can be used to compose probabilistic games in parallel and sequentially. We also consider morphisms between games, and show that intuitive constructions gi…
▽ More
We extend the open games framework for compositional game theory to encompass also mixed strategies, making essential use of the discrete probability distribution monad. We show that the resulting games form a symmetric monoidal category, which can be used to compose probabilistic games in parallel and sequentially. We also consider morphisms between games, and show that intuitive constructions give rise to functors and adjunctions between pure and probabilistic open games.
△ Less
Submitted 14 September, 2020;
originally announced September 2020.
-
Suspended graphene membranes with attached silicon proof masses as piezoresistive NEMS accelerometers
Authors:
Xuge Fan,
Fredrik Forsberg,
Anderson D. Smith,
Stephan Schröder,
Stefan Wagner,
Mikael Östling,
Max C. Lemme,
Frank Niklaus
Abstract:
Graphene is an atomically thin material that features unique electrical and mechanical properties, which makes it an extremely promising material for future nanoelectromechanical systems (NEMS). Recently, basic NEMS accelerometer functionality has been demonstrated by utilizing piezoresistive graphene ribbons with suspended silicon proof masses. However, the proposed graphene ribbons have limitati…
▽ More
Graphene is an atomically thin material that features unique electrical and mechanical properties, which makes it an extremely promising material for future nanoelectromechanical systems (NEMS). Recently, basic NEMS accelerometer functionality has been demonstrated by utilizing piezoresistive graphene ribbons with suspended silicon proof masses. However, the proposed graphene ribbons have limitations regarding mechanical robustness, manufacturing yield and the maximum measurement current that can be applied across the ribbons. Here, we report on suspended graphene membranes that are fully-clamped at their circumference and that have attached silicon proof masses. We demonstrate their utility as piezoresistive NEMS accelerometers and they are found to be more robust, have longer life span and higher manufacturing yield, can withstand higher measurement currents and are able to suspend larger silicon proof masses, as compared to the previously graphene ribbon devices. These findings are an important step towards bringing ultra-miniaturized piezoresistive graphene NEMS closer towards deployment in emerging applications such as in wearable electronics, biomedical implants and internet of things (IoT) devices.
△ Less
Submitted 16 March, 2020;
originally announced March 2020.
-
Manufacture and Characterization of Graphene Membranes with Suspended Silicon Proof Masses for MEMS and NEMS Applications
Authors:
Xuge Fan,
Anderson D. Smith,
Fredrik Forsberg,
Stefan Wagner,
Stephan Schröder,
Sayedeh Shirin Afyouni Akbari,
Andreas C. Fischer,
Luis Guillermo Villanueva,
Mikael Östling,
Max C. Lemme,
Frank Niklaus
Abstract:
Unparalleled strength, chemical stability, ultimate surface-to-volume ratio and excellent electronic properties of graphene make it an ideal candidate as a material for membranes in micro- and nanoelectromechanical systems (MEMS and NEMS). However, the integration of graphene into MEMS or NEMS devices and suspended structures such as proof masses on graphene membranes raises several technological…
▽ More
Unparalleled strength, chemical stability, ultimate surface-to-volume ratio and excellent electronic properties of graphene make it an ideal candidate as a material for membranes in micro- and nanoelectromechanical systems (MEMS and NEMS). However, the integration of graphene into MEMS or NEMS devices and suspended structures such as proof masses on graphene membranes raises several technological challenges, including collapse and rupture of the graphene. We have developed a robust route for realizing membranes made of double-layer CVD graphene and suspending large silicon proof masses on membranes with high yields. We have demonstrated the manufacture of square graphene membranes with side lengths from 7 micro meter to 110 micro meter and suspended proof masses consisting of solid silicon cubes that are from 5 micro meter multiply 5 micro meter multiply 16.4 micro meter to 100 micro meter multiply 100 micro meter multiply 16.4 micro meter in size. Our approach is compatible with wafer-scale MEMS and semiconductor manufacturing technologies, and the manufacturing yields of the graphene membranes with suspended proof masses were greater than 90%, with more than 70% of the graphene membranes having more than 90% graphene area without visible defects. The graphene membranes with suspended proof masses were extremely robust and were able to withstand indentation forces from an atomic force microscope (AFM) tip of up to ~7000 nN. The measured resonance frequencies of the realized structures ranged from tens to hundreds of kHz, with quality factors ranging from 63 to 148. The proposed approach for the reliable and large-scale manufacture of graphene membranes with suspended proof masses will enable the development and study of innovative NEMS devices with new functionalities and improved performances.
△ Less
Submitted 16 March, 2020;
originally announced March 2020.
-
Graphene ribbons with suspended masses as transducers in ultra-small nanoelectromechanical accelerometers
Authors:
Xuge Fan,
Fredrik Forsberg,
Anderson D. Smith,
Stephan Schröder,
Stefan Wagner,
Henrik Rödjegård,
Andreas C. Fischer,
Mikael Östling,
Max C. Lemme,
Frank Niklaus
Abstract:
Nanoelectromechanical system (NEMS) sensors and actuators could be of use in the development of next generation mobile, wearable, and implantable devices. However, these NEMS devices require transducers that are ultra-small, sensitive and can be fabricated at low cost. Here, we show that suspended double-layer graphene ribbons with attached silicon proof masses can be used as combined spring-mass…
▽ More
Nanoelectromechanical system (NEMS) sensors and actuators could be of use in the development of next generation mobile, wearable, and implantable devices. However, these NEMS devices require transducers that are ultra-small, sensitive and can be fabricated at low cost. Here, we show that suspended double-layer graphene ribbons with attached silicon proof masses can be used as combined spring-mass and piezoresistive transducers. The transducers, which are realized using processes that are compatible with large-scale semiconductor manufacturing technologies, can yield NEMS accelerometers that occupy at least two orders of magnitude smaller die area than conventional state-of-the-art silicon accelerometers.
△ Less
Submitted 16 March, 2020;
originally announced March 2020.
-
Three Equivalent Ordinal Notation Systems in Cubical Agda
Authors:
Fredrik Nordvall Forsberg,
Chuangjie Xu,
Neil Ghani
Abstract:
We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so…
▽ More
We present three ordinal notation systems representing ordinals below $\varepsilon_0$ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.
△ Less
Submitted 2 January, 2020; v1 submitted 24 April, 2019;
originally announced April 2019.
-
Catalog of Optimization Strategies and Realizations for Composed Integration Patterns
Authors:
Daniel Ritter,
Fredrik Nordvall Forsberg,
Stefanie Rinderle-Ma,
Norman May
Abstract:
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of Enterprise Integration Patterns (EIPs), are only informally described, and thus their composition takes place in an informal, ad-hoc manner. This leads to several issues…
▽ More
The discipline of Enterprise Application Integration (EAI) is the centrepiece of current on-premise, cloud and device integration scenarios. However, the building blocks of integration scenarios, i.e., essentially a composition of Enterprise Integration Patterns (EIPs), are only informally described, and thus their composition takes place in an informal, ad-hoc manner. This leads to several issues including a currently missing optimization of application integration scenarios. In this work, we collect and briefly explain the usage of process optimizations from the literature for integration scenario processes as catalog.
△ Less
Submitted 4 January, 2019;
originally announced January 2019.
-
A Compositional Treatment of Iterated Open Games
Authors:
Neil Ghani,
Clemens Kupke,
Alasdair Lambert,
Fredrik Nordvall Forsberg
Abstract:
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra sem…
▽ More
Compositional Game Theory is a new, recently introduced model of economic games based upon the computer science idea of compositionality. In it, complex and irregular games can be built up from smaller and simpler games, and the equilibria of these complex games can be defined recursively from the equilibria of their simpler subgames. This paper extends the model by providing a final coalgebra semantics for infinite games. In the course of this, we introduce a new operator on games to model the economic concept of subgame perfection.
△ Less
Submitted 21 November, 2017;
originally announced November 2017.
-
Piezoresistive Properties of Suspended Graphene Membranes under Uniaxial and Biaxial Strain in Nanoelectromechanical Pressure Sensors
Authors:
Anderson D. Smith,
Frank Niklaus,
Alan Paussa,
Stephan Schröder,
Andreas C. Fischer,
Mikael Sterner,
Stefan Wagner,
Sam Vaziri,
Fredrik Forsberg,
David Esseni,
Mikael Östling,
Max C. Lemme
Abstract:
Graphene membranes act as highly sensitive transducers in nanoelectromechanical devices due to their ultimate thinness. Previously, the piezoresistive effect has been experimentally verified in graphene using uniaxial strain in graphene. Here we report experimental and theoretical data on the uni- and biaxial piezoresistive properties of suspended graphene membranes applied to piezoresistive press…
▽ More
Graphene membranes act as highly sensitive transducers in nanoelectromechanical devices due to their ultimate thinness. Previously, the piezoresistive effect has been experimentally verified in graphene using uniaxial strain in graphene. Here we report experimental and theoretical data on the uni- and biaxial piezoresistive properties of suspended graphene membranes applied to piezoresistive pressure sensors. A detailed model that utilizes a linearized Boltzman transport equation describes accurately the charge carrier density and mobility in strained graphene, and hence the gauge factor. The gauge factor is found to be practically independent of the doping concentration and crystallographic orientation of the graphene films. These investigations provide deeper insight into the piezoresistive behavior of graphene membranes.
△ Less
Submitted 13 August, 2017;
originally announced August 2017.
-
Quotient inductive-inductive types
Authors:
Thorsten Altenkirch,
Paolo Capriotti,
Gabe Dijkstra,
Nicolai Kraus,
Fredrik Nordvall Forsberg
Abstract:
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of HoTT (i.e. do not satisfy uniqueness of equality proofs) such as spheres, suspensions and the torus. However, there are also interesting uses of HITs t…
▽ More
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of HoTT (i.e. do not satisfy uniqueness of equality proofs) such as spheres, suspensions and the torus. However, there are also interesting uses of HITs to define sets, such as the Cauchy reals, the partiality monad, and the internal, total syntax of type theory. In each of these examples we define several types that depend on each other mutually, i.e. they are inductive-inductive definitions. We call those HITs quotient inductive-inductive types (QIITs).
Although there has been recent progress on the general theory of HITs, there isn't yet a theoretical foundation of the combination of equality constructors and induction-induction, despite having many interesting applications. In the present paper we present a first step towards a semantic definition of QIITs. In particular, we give an initial-algebra semantics and show that this is equivalent to the section induction principle, which justifies the intuitively expected elimination rules.
△ Less
Submitted 16 November, 2017; v1 submitted 7 December, 2016;
originally announced December 2016.
-
Precision measurements of Linear Scattering Density using Muon Tomography
Authors:
E. Åström,
G. Bonomi,
I. Calliari,
P. Calvini,
P. Checchia,
A. Donzella,
E. Faraci,
F. Forsberg,
F. Gonella,
X. Hu,
J. Klinger,
L. Sundqvist Ödqvist,
D. Pagano,
A. Rigoni,
E. Ramous,
M. Urbani,
S. Vanini,
A. Zenoni,
G. Zumerle
Abstract:
We demonstrate that muon tomography can be used to precisely measure the properties of various materials. The materials which have been considered have been extracted from an experimental blast furnace, including carbon (coke) and iron oxides, for which measurements of the linear scattering density relative to the mass density have been performed with an absolute precision of 10%. We report the pr…
▽ More
We demonstrate that muon tomography can be used to precisely measure the properties of various materials. The materials which have been considered have been extracted from an experimental blast furnace, including carbon (coke) and iron oxides, for which measurements of the linear scattering density relative to the mass density have been performed with an absolute precision of 10%. We report the procedures that are used in order to obtain such precision, and a discussion is presented to address the expected performance of the technique when applied to heavier materials. The results we obtain do not depend on the specific type of material considered and therefore they can be extended to any application.
△ Less
Submitted 22 July, 2016; v1 submitted 24 May, 2016;
originally announced May 2016.
-
Integrating MEMS and ICs
Authors:
Andreas C. Fischer,
Fredrik Forsberg,
Martin Lapisa,
Simon J. Bleiker,
Goran Stemme,
Niclas Roxhed,
Frank Niklaus
Abstract:
The majority of microelectromechanical system (MEMS) devices must be combined with integrated circuits (ICs) for operation in larger electronic systems. While MEMS transducers sense or control physical, optical or chemical quantities, ICs typically provide functionalities related to the signals of these transducers, such as analog-to-digital conversion, amplification, filtering and information pro…
▽ More
The majority of microelectromechanical system (MEMS) devices must be combined with integrated circuits (ICs) for operation in larger electronic systems. While MEMS transducers sense or control physical, optical or chemical quantities, ICs typically provide functionalities related to the signals of these transducers, such as analog-to-digital conversion, amplification, filtering and information processing as well as communication between the MEMS transducer and the outside world. Thus, the vast majority of commercial MEMS products, such as accelerometers, gyroscopes and micro-mirror arrays, are integrated and packaged together with ICs. There are a variety of possible methods of integrating and packaging MEMS and IC components, and the technology of choice strongly depends on the device, the field of application and the commercial requirements. In this review paper, traditional as well as innovative and emerging approaches to MEMS and IC integration are reviewed. These include approaches based on the hybrid integration of multiple chips (multi-chip solutions) as well as system-on-chip solutions based on wafer-level monolithic integration and heterogeneous integration techniques. These are important technological building blocks for the More-Than-Moore paradigm described in the International Technology Roadmap for Semiconductors. In this paper, the various approaches are categorized in a coherent manner, their merits are discussed, and suitable application areas and implementations are critically investigated. The implications of the different MEMS and IC integration approaches for packaging, testing and final system costs are reviewed.
△ Less
Submitted 17 April, 2016;
originally announced April 2016.
-
Resistive Graphene Humidity Sensors with Rapid and Direct Electrical Readout
Authors:
Anderson David Smith,
Karim Elgammal,
Frank Niklaus,
Anna Delin,
Andreas Fischer,
Sam Vaziri,
Fredrik Forsberg,
Mikael Råsander,
Håkan W. Hugosson,
Lars Bergqvist,
Stephan Schröder,
Satender Kataria,
Mikael Östling,
Max C. Lemme
Abstract:
We demonstrate humidity sensing using a change of electrical resistance of a single- layer chemical vapor deposited (CVD) graphene that is placed on top of a SiO2 layer on a Si wafer. To investigate the selectivity of the sensor towards the most common constituents in air, its signal response was characterized individually for water vapor (H2O), nitrogen (N2), oxygen (O2), and argon (Ar). In order…
▽ More
We demonstrate humidity sensing using a change of electrical resistance of a single- layer chemical vapor deposited (CVD) graphene that is placed on top of a SiO2 layer on a Si wafer. To investigate the selectivity of the sensor towards the most common constituents in air, its signal response was characterized individually for water vapor (H2O), nitrogen (N2), oxygen (O2), and argon (Ar). In order to assess the humidity sensing effect for a range from 1% relative humidity (RH) to 96% RH, devices were characterized both in a vacuum chamber and in a humidity chamber at atmospheric pressure. The measured response and recovery times of the graphene humidity sensors are on the order of several hundred milliseconds. Density functional theory simulations are employed to further investigate the sensitivity of the graphene devices towards water vapor. Results from the interaction between the electrostatic dipole moment of the water and the impurity bands in the SiO2 substrate, which in turn leads to electrostatic doping of the graphene layer. The proposed graphene sensor provides rapid response direct electrical read out and is compatible with back end of the line (BEOL) integration on top of CMOS-based integrated circuits.
△ Less
Submitted 25 October, 2015;
originally announced October 2015.
-
Positive Inductive-Recursive Definitions
Authors:
Neil Ghani,
Fredrik Nordvall Forsberg,
Lorenzo Malatesta
Abstract:
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a…
▽ More
A new theory of data types which allows for the definition of types as initial algebras of certain functors Fam(C) -> Fam(C) is presented. This theory, which we call positive inductive-recursive definitions, is a generalisation of Dybjer and Setzer's theory of inductive-recursive definitions within which C had to be discrete -- our work can therefore be seen as lifting this restriction. This is a substantial endeavour as we need to not only introduce a type of codes for such data types (as in Dybjer and Setzer's work), but also a type of morphisms between such codes (which was not needed in Dybjer and Setzer's development). We show how these codes are interpreted as functors on Fam(C) and how these morphisms of codes are interpreted as natural transformations between such functors. We then give an application of positive inductive-recursive definitions to the theory of nested data types and we give concrete examples of recursive functions defined on universes by using their elimination principle. Finally we justify the existence of positive inductive-recursive definitions by adapting Dybjer and Setzer's set-theoretic model to our setting.
△ Less
Submitted 26 March, 2015; v1 submitted 19 February, 2015;
originally announced February 2015.
-
Extracting verified decision procedures: DPLL and Resolution
Authors:
Ulrich Berger,
Andrew Lawrence,
Fredrik Nordvall Forsberg,
Monika Seisenberger
Abstract:
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form th…
▽ More
This article is concerned with the application of the program extraction technique to a new class of problems: the synthesis of decision procedures for the classical satisfiability problem that are correct by construction. To this end, we formalize a completeness proof for the DPLL proof system and extract a SAT solver from it. When applied to a propositional formula in conjunctive normal form the program produces either a satisfying assignment or a DPLL derivation showing its unsatisfiability. We use non-computational quantifiers to remove redundant computational content from the extracted program and translate it into Haskell to improve performance. We also prove the equivalence between the resolution proof system and the DPLL proof system with a bound on the size of the resulting resolution proof. This demonstrates that it is possible to capture quantitative information about the extracted program on the proof level. The formalization is carried out in the interactive proof assistant Minlog.
△ Less
Submitted 8 March, 2015; v1 submitted 7 February, 2015;
originally announced February 2015.
-
Electromechanical Piezoresistive Sensing in Suspended Graphene Membranes
Authors:
A. D. Smith,
F. Niklaus,
A. Paussa,
S. Vaziri,
A. C. Fischer,
M. Sterner,
F. Forsberg,
A. Delin,
D. Esseni,
P. Palestri,
M. Östling,
M. C. Lemme
Abstract:
Monolayer graphene exhibits exceptional electronic and mechanical properties, making it a very promising material for nanoelectromechanical (NEMS) devices. Here, we conclusively demonstrate the piezoresistive effect in graphene in a nano-electromechanical membrane configuration that provides direct electrical readout of pressure to strain transduction. This makes it highly relevant for an importan…
▽ More
Monolayer graphene exhibits exceptional electronic and mechanical properties, making it a very promising material for nanoelectromechanical (NEMS) devices. Here, we conclusively demonstrate the piezoresistive effect in graphene in a nano-electromechanical membrane configuration that provides direct electrical readout of pressure to strain transduction. This makes it highly relevant for an important class of nano-electromechanical system (NEMS) transducers. This demonstration is consistent with our simulations and previously reported gauge factors and simulation values. The membrane in our experiment acts as a strain gauge independent of crystallographic orientation and allows for aggressive size scalability. When compared with conventional pressure sensors, the sensors have orders of magnitude higher sensitivity per unit area.
△ Less
Submitted 25 June, 2013;
originally announced June 2013.
-
Characterization and Predictive Modeling of Epitaxial Silicon-Germanium Thermistor Layers
Authors:
B. Gunnar Malm,
Mohammadreza Kolahdouz,
Fredrik Forsberg,
Frank Niklaus
Abstract:
The thermal coefficient of resistance (TCR) for epitaxial silicon-germanium (SiGe) layers has been analyzed by experiment and simulation. Predictive simulation using drift-diffusion formalism and self-consistent quantum-mechanical solutions yielded similar results, TCR around 2%/K at 300 K. This modeling approach can be used for different, graded and constant, SiGe profiles,. It is also capable of…
▽ More
The thermal coefficient of resistance (TCR) for epitaxial silicon-germanium (SiGe) layers has been analyzed by experiment and simulation. Predictive simulation using drift-diffusion formalism and self-consistent quantum-mechanical solutions yielded similar results, TCR around 2%/K at 300 K. This modeling approach can be used for different, graded and constant, SiGe profiles,. It is also capable of predicting the influence of background auto-doping on the TCR of the detectors
△ Less
Submitted 9 December, 2011;
originally announced December 2011.
