Open Access. Powered by Scholars. Published by Universities.®

Computer Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

Articles 1 - 30 of 65

Full-Text Articles in Computer Engineering

Multi-Scale Attention Networks For Pavement Defect Detection, Junde Chen, Yuxin Wen, Yaser Ahangari Nanehkaran, Defu Zhang, Adan Zeb Jul 2023

Multi-Scale Attention Networks For Pavement Defect Detection, Junde Chen, Yuxin Wen, Yaser Ahangari Nanehkaran, Defu Zhang, Adan Zeb

Engineering Faculty Articles and Research

Pavement defects such as cracks, net cracks, and pit slots can cause potential traffic safety problems. The timely detection and identification play a key role in reducing the harm of various pavement defects. Particularly, the recent development in deep learning-based CNNs has shown competitive performance in image detection and classification. To detect pavement defects automatically and improve effects, a multi-scale mobile attention-based network, which we termed MANet, is proposed to perform the detection of pavement defects. The architecture of the encoder-decoder is used in MANet, where the encoder adopts the MobileNet as the backbone network to extract pavement defect features. …


Para Cima Y Pa’ Abajo: Building Bridges Between Hci Research In Latin America And In The Global North, Pedro Reynolds-Cuéllar, Marisol Wong-Villacres, Karla A. Badillo-Urquiola, Mayra Donaji Barrera-Machuca, Franceli L. Cibrian, Marianela Ciolfi Felice, Carolina Fuentes, Laura Sanely Gaytán-Lugo, Vivian Genaro Motti, Monica Perusquía-Hernández, Oscar A. Lemus Apr 2023

Para Cima Y Pa’ Abajo: Building Bridges Between Hci Research In Latin America And In The Global North, Pedro Reynolds-Cuéllar, Marisol Wong-Villacres, Karla A. Badillo-Urquiola, Mayra Donaji Barrera-Machuca, Franceli L. Cibrian, Marianela Ciolfi Felice, Carolina Fuentes, Laura Sanely Gaytán-Lugo, Vivian Genaro Motti, Monica Perusquía-Hernández, Oscar A. Lemus

Engineering Faculty Articles and Research

The Human-computer Interaction (HCI) community has the opportunity to foster the integration of research practices across the Global South and North to begin overcoming colonial relationships. In this paper, we focus on the case of Latin America (LATAM), where initiatives to increase the representation of HCI practitioners lack a consolidated understanding of the practices they employ, the factors that influence them, and the challenges that practitioners face. To address this knowledge gap, we employ a mixed-methods approach, comprising a survey (66 respondents) and in-depth interviews (19 interviewees). Our analyses characterize a set of research perspectives on how HCI is practiced …


Completeness Of Nominal Props, Samuel Balco, Alexander Kurz Jan 2023

Completeness Of Nominal Props, Samuel Balco, Alexander Kurz

Engineering Faculty Articles and Research

We introduce nominal string diagrams as string diagrams internal in the category of nominal sets. This leads us to define nominal PROPs and nominal monoidal theories. We show that the categories of ordinary PROPs and nominal PROPs are equivalent. This equivalence is then extended to symmetric monoidal theories and nominal monoidal theories, which allows us to transfer completeness results between ordinary and nominal calculi for string diagrams.


Towards Qos-Based Embedded Machine Learning, Tom Springer, Erik Linstead, Peiyi Zhao, Chelsea Parlett-Pelleriti Oct 2022

Towards Qos-Based Embedded Machine Learning, Tom Springer, Erik Linstead, Peiyi Zhao, Chelsea Parlett-Pelleriti

Engineering Faculty Articles and Research

Due to various breakthroughs and advancements in machine learning and computer architectures, machine learning models are beginning to proliferate through embedded platforms. Some of these machine learning models cover a range of applications including computer vision, speech recognition, healthcare efficiency, industrial IoT, robotics and many more. However, there is a critical limitation in implementing ML algorithms efficiently on embedded platforms: the computational and memory expense of many machine learning models can make them unsuitable in resource-constrained environments. Therefore, to efficiently implement these memory-intensive and computationally expensive algorithms in an embedded computing environment, innovative resource management techniques are required at the …


Machine Learning Based Medical Image Deepfake Detection: A Comparative Study, Siddharth Solaiyappan, Yuxin Wen Apr 2022

Machine Learning Based Medical Image Deepfake Detection: A Comparative Study, Siddharth Solaiyappan, Yuxin Wen

Engineering Faculty Articles and Research

Deep generative networks in recent years have reinforced the need for caution while consuming various modalities of digital information. One avenue of deepfake creation is aligned with injection and removal of tumors from medical scans. Failure to detect medical deepfakes can lead to large setbacks on hospital resources or even loss of life. This paper attempts to address the detection of such attacks with a structured case study. Specifically, we evaluate eight different machine learning algorithms, which include three conventional machine learning methods (Support Vector Machine, Random Forest, Decision Tree) and five deep learning models (DenseNet121, DenseNet201, ResNet50, ResNet101, VGG19) …


A Deep Learning-Based Approach To Extraction Of Filler Morphology In Sem Images With The Application Of Automated Quality Inspection, Md. Fashiar Rahman, Tzu-Liang Bill Tseng, Jianguo Wu, Yuxin Wen, Yirong Lin Mar 2022

A Deep Learning-Based Approach To Extraction Of Filler Morphology In Sem Images With The Application Of Automated Quality Inspection, Md. Fashiar Rahman, Tzu-Liang Bill Tseng, Jianguo Wu, Yuxin Wen, Yirong Lin

Engineering Faculty Articles and Research

Automatic extraction of filler morphology (size, orientation, and spatial distribution) in Scanning Electron Microscopic (SEM) images is essential in many applications such as automatic quality inspection in composite manufacturing. Extraction of filler morphology greatly depends on accurate segmentation of fillers (fibers and particles), which is a challenging task due to the overlap of fibers and particles and their obscure presence in SEM images. Convolution Neural Networks (CNNs) have been shown to be very effective at object recognition in digital images. This paper proposes an automatic filler detection system in SEM images, utilizing a Mask Region-based CNN architecture. The proposed system …


Three Wave Mixing In Epsilon-Near-Zero Plasmonic Waveguides For Signal Regeneration, Nicholas Mirchandani, Mark C. Harrison Mar 2022

Three Wave Mixing In Epsilon-Near-Zero Plasmonic Waveguides For Signal Regeneration, Nicholas Mirchandani, Mark C. Harrison

Engineering Faculty Articles and Research

Vast improvements in communications technology are possible if the conversion of digital information from optical to electric and back can be removed. Plasmonic devices offer one solution due to optical computing’s potential for increased bandwidth, which would enable increased throughput and enhanced security. Plasmonic devices have small footprints and interface with electronics easily, but these potential improvements are offset by the large device footprints of conventional signal regeneration schemes, since surface plasmon polaritons (SPPs) are incredibly lossy. As such, there is a need for novel regeneration schemes. The continuous, uniform, and unambiguous digital information encoding method is phase-shift-keying (PSK), so …


Let's Read: Designing A Smart Display Application To Support Codas When Learning Spoken Language, Katie Rodeghiero, Yingying Yuki Chen, Annika M. Hettmann, Franceli L. Cibrian Nov 2021

Let's Read: Designing A Smart Display Application To Support Codas When Learning Spoken Language, Katie Rodeghiero, Yingying Yuki Chen, Annika M. Hettmann, Franceli L. Cibrian

Engineering Faculty Articles and Research

Hearing children of Deaf adults (CODAs) face many challenges including having difficulty learning spoken languages, experiencing social judgment, and encountering greater responsibilities at home. In this paper, we present a proposal for a smart display application called Let's Read that aims to support CODAs when learning spoken language. We conducted a qualitative analysis using online community content in English to develop the first version of the prototype. Then, we conducted a heuristic evaluation to improve the proposed prototype. As future work, we plan to use this prototype to conduct participatory design sessions with Deaf adults and CODAs to evaluate the …


Feel And Touch: A Haptic Mobile Game To Assess Tactile Processing, Ivonne Monarca, Monica Tentori, Franceli L. Cibrian Nov 2021

Feel And Touch: A Haptic Mobile Game To Assess Tactile Processing, Ivonne Monarca, Monica Tentori, Franceli L. Cibrian

Engineering Faculty Articles and Research

Haptic interfaces have great potential for assessing the tactile processing of children with Autism Spectrum Disorder (ASD), an area that has been under-explored due to the lack of tools to assess it. Until now, haptic interfaces for children have mostly been used as a teaching or therapeutic tool, so there are still open questions about how they could be used to assess tactile processing of children with ASD. This article presents the design process that led to the development of Feel and Touch, a mobile game augmented with vibrotactile stimuli to assess tactile processing. Our feasibility evaluation, with 5 children …


Hierarchical Scheduling For Real-Time Periodic Tasks In Symmetric Multiprocessing, Tom Springer, Peiyi Zhao Jun 2021

Hierarchical Scheduling For Real-Time Periodic Tasks In Symmetric Multiprocessing, Tom Springer, Peiyi Zhao

Engineering Faculty Articles and Research

In this paper, we present a new hierarchical scheduling framework for periodic tasks in symmetric multiprocessor (SMP) platforms. Partitioned and global scheduling are the two main approaches used by SMP based systems where global scheduling is recommended for overall performance and partitioned scheduling is recommended for hard real-time performance. Our approach combines both the global and partitioned approaches of traditional SMP-based schedulers to provide hard real-time performance guarantees for critical tasks and improved response times for soft real-time tasks. Implemented as part of VxWorks, the results are confirmed using a real-time benchmark application, where response times were improved for soft …


On-Device Deep Learning Inference For System-On-Chip (Soc) Architectures, Tom Springer, Elia Eiroa-Lledo, Elizabeth Stevens, Erik Linstead Mar 2021

On-Device Deep Learning Inference For System-On-Chip (Soc) Architectures, Tom Springer, Elia Eiroa-Lledo, Elizabeth Stevens, Erik Linstead

Engineering Faculty Articles and Research

As machine learning becomes ubiquitous, the need to deploy models on real-time, embedded systems will become increasingly critical. This is especially true for deep learning solutions, whose large models pose interesting challenges for target architectures at the “edge” that are resource-constrained. The realization of machine learning, and deep learning, is being driven by the availability of specialized hardware, such as system-on-chip solutions, which provide some alleviation of constraints. Equally important, however, are the operating systems that run on this hardware, and specifically the ability to leverage commercial real-time operating systems which, unlike general purpose operating systems such as Linux, can …


A Fortran-Keras Deep Learning Bridge For Scientific Computing, Jordan Ott, Mike Pritchard, Natalie Best, Erik Linstead, Milan Curcic, Pierre Baldi Aug 2020

A Fortran-Keras Deep Learning Bridge For Scientific Computing, Jordan Ott, Mike Pritchard, Natalie Best, Erik Linstead, Milan Curcic, Pierre Baldi

Engineering Faculty Articles and Research

Implementing artificial neural networks is commonly achieved via high-level programming languages such as Python and easy-to-use deep learning libraries such as Keras. These software libraries come preloaded with a variety of network architectures, provide autodifferentiation, and support GPUs for fast and efficient computation. As a result, a deep learning practitioner will favor training a neural network model in Python, where these tools are readily available. However, many large-scale scientific computation projects are written in Fortran, making it difficult to integrate with modern deep learning methods. To alleviate this problem, we introduce a software library, the Fortran-Keras Bridge (FKB). This two-way …


Exploring The Efficacy Of Transfer Learning In Mining Image‑Based Software Artifacts, Natalie Best, Jordan Ott, Erik J. Linstead Aug 2020

Exploring The Efficacy Of Transfer Learning In Mining Image‑Based Software Artifacts, Natalie Best, Jordan Ott, Erik J. Linstead

Engineering Faculty Articles and Research

Background

Transfer learning allows us to train deep architectures requiring a large number of learned parameters, even if the amount of available data is limited, by leveraging existing models previously trained for another task. In previous attempts to classify image-based software artifacts in the absence of big data, it was noted that standard off-the-shelf deep architectures such as VGG could not be utilized due to their large parameter space and therefore had to be replaced by customized architectures with fewer layers. This proves to be challenging to empirical software engineers who would like to make use of existing architectures without …


Ml-Medic: A Preliminary Study Of An Interactive Visual Analysis Tool Facilitating Clinical Applications Of Machine Learning For Precision Medicine, Laura Stevens, David Kao, Jennifer Hall, Carsten Görg, Kaitlyn Abdo, Erik Linstead May 2020

Ml-Medic: A Preliminary Study Of An Interactive Visual Analysis Tool Facilitating Clinical Applications Of Machine Learning For Precision Medicine, Laura Stevens, David Kao, Jennifer Hall, Carsten Görg, Kaitlyn Abdo, Erik Linstead

Engineering Faculty Articles and Research

Accessible interactive tools that integrate machine learning methods with clinical research and reduce the programming experience required are needed to move science forward. Here, we present Machine Learning for Medical Exploration and Data-Inspired Care (ML-MEDIC), a point-and-click, interactive tool with a visual interface for facilitating machine learning and statistical analyses in clinical research. We deployed ML-MEDIC in the American Heart Association (AHA) Precision Medicine Platform to provide secure internet access and facilitate collaboration. ML-MEDIC’s efficacy for facilitating the adoption of machine learning was evaluated through two case studies in collaboration with clinical domain experts. A domain expert review was also …


Learning In The Machine: To Share Or Not To Share?, Jordan Ott, Erik Linstead, Nicholas Lahaye, Pierre Baldi Mar 2020

Learning In The Machine: To Share Or Not To Share?, Jordan Ott, Erik Linstead, Nicholas Lahaye, Pierre Baldi

Engineering Faculty Articles and Research

Weight-sharing is one of the pillars behind Convolutional Neural Networks and their successes. However, in physical neural systems such as the brain, weight-sharing is implausible. This discrepancy raises the fundamental question of whether weight-sharing is necessary. If so, to which degree of precision? If not, what are the alternatives? The goal of this study is to investigate these questions, primarily through simulations where the weight-sharing assumption is relaxed. Taking inspiration from neural circuitry, we explore the use of Free Convolutional Networks and neurons with variable connection patterns. Using Free Convolutional Networks, we show that while weight-sharing is a pragmatic optimization …


Vrsensory: Designing Inclusive Virtual Games With Neurodiverse Children, Ben Wasserman, Derek Prate, Bryce Purnell, Alex Muse, Kaitlyn Abdo, Kendra Day, Louanne Boyd Oct 2019

Vrsensory: Designing Inclusive Virtual Games With Neurodiverse Children, Ben Wasserman, Derek Prate, Bryce Purnell, Alex Muse, Kaitlyn Abdo, Kendra Day, Louanne Boyd

Engineering Faculty Articles and Research

We explore virtual environments and accompanying interaction styles to enable inclusive play. In designing games for three neurodiverse children, we explore how designing for sensory diversity can be understood through a formal game design framework. Our process reveals that by using sensory processing needs as requirements we can make sensory and social accessible play spaces. We contribute empirical findings for accommodating sensory differences for neurodiverse children in a way that supports inclusive play. Specifically, we detail the sensory driven design choices that not only support the enjoyability of the leisure activities, but that also support the social inclusion of sensory-diverse …


Low-Energy Acceleration Of Binarized Convolutional Neural Networks Using A Spin Hall Effect Based Logic-In-Memory Architecture, Ashkan Samiee, Payal Borulkar, Ronald F. Demara, Peiyi Zhao, Yu Bai May 2019

Low-Energy Acceleration Of Binarized Convolutional Neural Networks Using A Spin Hall Effect Based Logic-In-Memory Architecture, Ashkan Samiee, Payal Borulkar, Ronald F. Demara, Peiyi Zhao, Yu Bai

Engineering Faculty Articles and Research

Deep Learning (DL) offers the advantages of high accuracy performance at tasks such as image recognition, learning of complex intelligent behaviors, and large-scale information retrieval problems such as intelligent web search. To attain the benefits of DL, the high computational and energy-consumption demands imposed by the underlying processing, interconnect, and memory devices on which software-based DL executes can benefit substantially from innovative hardware implementations. Logic-in-Memory (LIM) architectures offer potential approaches to attaining such throughput goals within area and energy constraints starting with the lowest layers of the hardware stack. In this paper, we develop a Spintronic Logic-in-Memory (S-LIM) XNOR neural …


Paper Prototyping Comfortable Vr Play For Diverse Sensory Needs, Louanne E. Boyd, Kendra Day, Ben Wasserman, Kaitlyn Abdo, Gillian Hayes, Erik J. Linstead May 2019

Paper Prototyping Comfortable Vr Play For Diverse Sensory Needs, Louanne E. Boyd, Kendra Day, Ben Wasserman, Kaitlyn Abdo, Gillian Hayes, Erik J. Linstead

Engineering Faculty Articles and Research

We co-designed paper prototype dashboards for virtual environments for three children with diverse sensory needs. Our goal was to determine individual interaction styles in order to enable comfortable and inclusive play. As a first step towards an inclusive virtual world, we began with designing for three sensory-diverse children who have labels of neurotypical, ADHD, and autism respectively. We focused on their leisure interests and their individual sensory profiles. We present the results of co-design with family members and paper prototyping sessions conducted by family members with the children. The results contribute preliminary empirical findings for accommodating different levels of engagement …


Applications Of Supervised Machine Learning In Autism Spectrum Disorder Research: A Review, Kayleigh K. Hyde, Marlena N. Novack, Nicholas Lahaye, Chelsea Parlett-Pelleriti, Raymond Anden, Dennis R. Dixon, Erik Linstead Feb 2019

Applications Of Supervised Machine Learning In Autism Spectrum Disorder Research: A Review, Kayleigh K. Hyde, Marlena N. Novack, Nicholas Lahaye, Chelsea Parlett-Pelleriti, Raymond Anden, Dennis R. Dixon, Erik Linstead

Engineering Faculty Articles and Research

Autism spectrum disorder (ASD) research has yet to leverage "big data" on the same scale as other fields; however, advancements in easy, affordable data collection and analysis may soon make this a reality. Indeed, there has been a notable increase in research literature evaluating the effectiveness of machine learning for diagnosing ASD, exploring its genetic underpinnings, and designing effective interventions. This paper provides a comprehensive review of 45 papers utilizing supervised machine learning in ASD, including algorithms for classification and text analysis. The goal of the paper is to identify and describe supervised machine learning trends in ASD literature as …


Exploring Age-Related Metamemory Differences Using Modified Brier Scores And Hierarchical Clustering, Chelsea Parlett-Pelleriti, Grace C. Lin, Masha R. Jones, Erik Linstead, Susanne M. Jaeggi Jan 2019

Exploring Age-Related Metamemory Differences Using Modified Brier Scores And Hierarchical Clustering, Chelsea Parlett-Pelleriti, Grace C. Lin, Masha R. Jones, Erik Linstead, Susanne M. Jaeggi

Engineering Faculty Articles and Research

Older adults (OAs) typically experience memory failures as they age. However, with some exceptions, studies of OAs’ ability to assess their own memory functions—Metamemory (MM)— find little evidence that this function is susceptible to age-related decline. Our study examines OAs’ and young adults’ (YAs) MM performance and strategy use. Groups of YAs (N = 138) and OAs (N = 79) performed a MM task that required participants to place bets on how likely they were to remember words in a list. Our analytical approach includes hierarchical clustering, and we introduce a new measure of MM—the modified Brier—in order to adjust …


Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz Jan 2017

Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz

Engineering Faculty Articles and Research

We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets.

We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).


Features Of Agent-Based Models, Reiko Heckel, Alexander Kurz, Edmund Chattoe-Brown Jan 2017

Features Of Agent-Based Models, Reiko Heckel, Alexander Kurz, Edmund Chattoe-Brown

Engineering Faculty Articles and Research

The design of agent-based models (ABMs) is often ad-hoc when it comes to defining their scope. In order for the inclusion of features such as network structure, location, or dynamic change to be justified, their role in a model should be systematically analysed. We propose a mechanism to compare and assess the impact of such features. In particular we are using techniques from software engineering and semantics to support the development and assessment of ABMs, such as graph transformations as semantic representations for agent-based models, feature diagrams to identify ingredients under consideration, and extension relations between graph transformation systems to …


Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz Jan 2017

Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz

Engineering Faculty Articles and Research

The second Dagstuhl seminar on coalgebraic logics took place from October 7-12, 2012, in the Leibniz Forschungszentrum Schloss Dagstuhl, following a successful earlier one in December 2009. From the 44 researchers who attended and the 30 talks presented, this collection highlights some of the progress that has been made in the field. We are grateful to Giuseppe Longo and his interest in a special issue in Mathematical Structures in Computer Science.


The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz Jan 2017

The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz

Engineering Faculty Articles and Research

We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos->Pos from an endofunctor T: Set->Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntax-building functor L': DL->DL from a syntax-building functor L: BA->BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case …


Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić Jan 2016

Multi-Type Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić

Engineering Faculty Articles and Research

In the present paper, we introduce a multi-type display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The displayapproach is suitable to modularly chart the space of dynamic epistemic logics on weaker-than-classical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth proof-theoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures Baltag-Moss-Solecki’s dynamic epistemic logic, and enjoys Belnap-style cut …


Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano Jan 2016

Multi-Type Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.


Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano Jan 2016

Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano

Engineering Faculty Articles and Research

We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, …


Extensions Of Functors From Set To V-Cat, Adriana Balan, Alexander Kurz, Jirí Velebil Jan 2015

Extensions Of Functors From Set To V-Cat, Adriana Balan, Alexander Kurz, Jirí Velebil

Engineering Faculty Articles and Research

We show that for a commutative quantale V every functor Set --> V-cat has an enriched left- Kan extension. As a consequence, coalgebras over Set are subsumed by coalgebras over V-cat. Moreover, one can build functors on V-cat by equipping Set-functors with a metric.


Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil Jan 2015

Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil

Engineering Faculty Articles and Research

Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weak-pullback preserving functors. To facilitate this analysis we prove a number of category theoretic results on …


Approximation Of Nested Fixpoints, Alexander Kurz Jan 2015

Approximation Of Nested Fixpoints, Alexander Kurz

Engineering Faculty Articles and Research

The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2-categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is …