جست‌وجوی استاد و پژوهشگر

Patrik Janssonمشاهده پروفایل

استاد

• Programming Languages
• Functional Programming
• Domain-Specific Languages
• +۴ مورد دیگر

Patrik Jansson is a Professor of Computer Science in the Department of Computer Science and Engineering at Chalmers University of Technology and the University of Gothenburg. He holds a PhD and MSc from Chalmers. As a Visiting Fellow of Kellogg College since 2024, he collaborates with Prof Jeremy Gibbons. His research focuses on programming languages, functional programming, and domain-specific languages, aiming to construct correct and reusable software systems. Applications span climate impact research, language technology, and foundational type theory. His recent work includes Bayesian optimization for fusion reactor disruptions and formal methods in sequential decision problems. Education: PhD in Computer Science, Chalmers University MSc in Computer Science, Chalmers University Research Interests: Patrik explores domain-specific languages (DSLs) for mathematics and scientific computing, leveraging functional programming paradigms. His work emphasizes rigorous type systems, formal verification, and the application of programming language theory to real-world challenges like climate modeling and fusion energy research. Current projects include optimizing plasma disruptions in tokamaks and developing DSL frameworks for uncertainty-aware decision-making. Grants & Collaborations: His research has received prestigious grants, including involvement in initiatives like CHAIR (Chalmers AI Research Centre) and collaborations with industry partners such as Volvo Cars and Sahlgrenska University Hospital. He contributes to cross-disciplinary efforts in AI-driven health technologies and distributed systems. Labs & Teams: Active in the Computer and Network Systems division, focusing on high-performance computing, secure communication, and embedded systems. He co-leads projects on AI security and health engineering through the Chalmers Sahlgrenska Health Engineering Alliance.

• Philosophy
• Logic
• Philosophy of Mathematics
• +۳ مورد دیگر

Tim Button is a Professor of Philosophy & Logic at the Department of Philosophy, University College London (UCL). Previously, he held academic roles at the University of Cambridge, including as a PhD student (2006–2010), research fellow (2010–2012), and faculty member (2012–2019). His research focuses on philosophy of mathematics, formal logic, set theory, and metaphysics. He has authored influential works on topics such as iterative concepts of set theory, alternative set theories, and fictionalism in metaphysics. Button is also known for developing textbooks like forall x: Calgary , which introduces formal logic to students. His recent publications explore foundational questions in mathematics and logic, including critiques of type theory and explorations of level theory as an axiomatic framework. Button has contributed to debates on model-theoretic arguments, computability, and the philosophy of Hilary Putnam. His work bridges formal methods with philosophical inquiry, emphasizing clarity and rigor in conceptual analysis. Research interests include: logic, set theory, philosophy of mathematics, formal ontology, metaphysical debates about universals, and the foundations of mathematics. His scholarship often intersects with technical logic and broader philosophical questions about truth, existence, and methodology. Notable contributions include critiques of cumulative type theory, the development of level theory as an alternative to traditional set theories, and analyses of model-theoretic skepticism. Button’s pedagogical efforts, such as open-access logic textbooks, aim to make formal methods accessible to a wider audience.

• Modeling and verification of reactive systems
• Probabilistic model checking
• Stochastic systems analysis
• +۷ مورد دیگر

Christel Baier is a full professor and head of the Chair for Algebraic and Logical Foundations of Computer Science at TU Dresden since 2006. She holds a Diploma in Mathematics (1990), PhD (1994), and Habilitation (1999) from the University of Mannheim. Previously, she was an associate professor at the University of Bonn (1999–2006). She serves as Dean of the Faculty of Computer Science at TU Dresden (2025–2027) and has held leadership roles including Vice-Dean (2019–2024). Her research focuses on formal methods, probabilistic systems, and verification, with notable contributions in probabilistic model checking, temporal logics, and automata theory. She has received prestigious awards such as the Honorary Doctorate from RWTH Aachen (2022) and the Jean-Claude Laprie Award (2023). She leads major projects like SEMECO (Zukunftscluster) and contributes to initiatives like the Collaborative Research Center for Tactile Internet. Her editorial roles include editorship of Acta Informatica and ACM SIGLOG News . Baier's work bridges theoretical foundations with practical applications in system dependability and software engineering. She actively participates in international conferences and program committees, emphasizing the synthesis and analysis of component-based systems.

• Theoretical Computer Science
• Lambda Calculus
• Combinatorial Logic
• +۳ مورد دیگر

Katarzyna Grygiel is a researcher in theoretical computer science at the Faculty of Mathematics and Computer Science, Jagiellonian University. Her primary affiliation is with the Department of Foundations of Informatics, where she focuses on lambda calculus, combinatorial logic, and asymptotic properties of formal systems. She earned her MSc in Mathematics (2007) and PhD in Computer Science (2013) from Jagiellonian University. Her research interests span lambda calculus, combinatorial analysis of formal systems, and the application of probabilistic methods to logic. She has contributed to understanding normalization properties in combinatory logic and developed algorithms for generating lambda terms using Boltzmann samplers. Her work bridges theoretical computer science with foundational mathematical logic. Key grants include leadership roles in projects like 'Asymptotic methods in lambda calculus and combinatorial logic' (2014–2017) and 'Quantitative Research in Logics and Computational Theory' (2009–2012). She co-organized major conferences, including the 27th International Conference on Probabilistic, Combinatorial and Asymptotic Methods for the Analysis of Algorithms (2016). Her publications emphasize combinatorial studies of lambda terms, foundational logic, and algorithmic methods. Collaborations include researchers at École Polytechnique and University of Paris, reflecting her international scholarly network.

• Algebra
• Computational Complexity
• Theoretical Computer Science
• +۳ مورد دیگر

Prof. Pawel M. Idziak is a distinguished academic at the Faculty of Mathematics and Computer Science, Jagiellonian University, where he holds a Professorship in the Department of Algorithmics. His primary research focuses on algebra, computational complexity, and theoretical computer science, with notable contributions to the study of algebraic structures, satisfiability problems, and modular circuits. Idziak has led and contributed to numerous grants, including managing the 'Numerical and Structural Invariants in Algebra, Logic and Constraint Satisfaction Problems' (2015–2022) and co-ordinating initiatives like 'Programmers of the Future 4.0'. His work bridges abstract algebra with computational challenges, addressing topics such as group theory, circuit satisfiability, and algorithmic complexity. His research interests span a broad spectrum of theoretical computer science and algebra, including the interplay between algebraic structures and computational problems. Idziak has advised over 20 PhD students, mentoring them in areas such as algorithm design, logic in computer science, and discrete mathematics. He has also contributed to foundational works like Generative Complexity in Algebra (2005) and co-authored influential papers in journals like SIAM Journal on Computing and Transactions of the American Mathematical Society . Idziak’s academic leadership is evident through his roles in institutional committees and his active participation in international conferences. His recent work (2024) on equation satisfiability in solvable groups highlights his ongoing contributions to advancing computational algebra and complexity theory.

• Constraint Satisfaction Problem
• Computational Complexity
• Universal Algebra
• +۳ مورد دیگر

Dr. hab. Marcin Kozik is a Professor at the Department of Algorithmics within the Faculty of Mathematics and Computer Science at Jagiellonian University. His research focuses on Constraint Satisfaction Problems (CSP), Universal Algebra, and Computational Complexity. He has led multiple grants including 'Constraint Satisfaction Problems: Beyond the Finite Case' (2022–2026) and organized AAA 101 conference (2022). His work bridges algebraic methods with computational complexity, contributing to foundational theories in CSP dichotomy and robust algorithms. Research interests include algebraic approaches to CSP, complexity of finite algebras, and robust algorithms for near-unanimity CSPs. Recent publications emphasize quantum CSP strategies, unifying algebraic frameworks, and injective hardness conditions. He has received awards for his habilitation research (2011) and contributions in 2021. Grants Managed: Topological Correction Codes in Error-Resistant Quantum Computing (2022–2026) "Constraint Satisfaction Problems: Beyond the Finite Case" (Ministry of Science & Higher Education, 2022–2026) Key Contributions: Over 35 peer-reviewed articles, including foundational work on bounded width CSPs and absorption theory in universal algebra. Labs/Teams: Part of the Algorithmics Research Group, collaborating with Libor Barto, Andrei Bulatov, and others on CSP and algebraic complexity.

Håkon Robbestad Gylterudمشاهده پروفایل

دانشیار

• Dependent Type Theory
• Homotopy Type Theory
• Logic in Computer Science
• +۹ مورد دیگر

Håkon Robbestad Gylterud is an Associate Professor in the Department of Informatics at the University of Bergen, Norway. His academic work bridges mathematics and computer science, with a strong focus on logical foundations and formal systems. University: University of Bergen School: Faculty of Mathematics and Natural Sciences Department: Department of Informatics Position: Associate Professor His research centers on dependent type theory and homotopy type theory (HoTT), aiming to formalize mathematical reasoning and computational structures. He explores foundational concepts such as multisets, iterative sets, and data structures with symmetries within type-theoretic frameworks. His interests extend to category theory, algebra, topology, and the computer formalization of mathematics, emphasizing constructivity and rigorous logical modeling. The recent publications highlight a consistent trend in applying homotopy type theory to diverse mathematical structures—ranging from multisets and sets to planar graphs and category-theoretic constructions. These works demonstrate a deep engagement with univalent foundations and higher-dimensional reasoning, contributing to the theoretical robustness of type systems. No scientific awards are explicitly mentioned in the provided texts. Håkon advises research through collaborative publications, particularly with scholars like Jonathan Cubides and Daniel Gratzer. While no formal grants are listed, his sustained research output suggests active funding and academic support. He leads or contributes to research groups such as the Programming Theory group at UiB. He is involved in several research projects, including Algebraic Type Theory, Multisets and Sets in HoTT, Quoting Operations, and the Anti-Pattern Game. These initiatives reflect both serious theoretical inquiry and creative, interdisciplinary exploration.

Michal Walickiمشاهده پروفایل

دانشیار

• Mathematical Logic
• Philosophical Logic
• Graph Theory
• +۱۳ مورد دیگر

Michal Walicki is an Associate Professor in the Department of Informatics at the University of Bergen, Norway. His research lies at the intersection of mathematical logic, theoretical computer science, and philosophy of logic. He specializes in graph-theoretic methods for analyzing logical paradoxes, paraconsistency, and the algebraic semantics of nondeterminism. His primary research interests include self-reference, semantic paradoxes, digraph kernels, paraconsistent logic, multialgebras, and bounded reasoning in epistemic logic. He has developed graph-based semantics for logical theories, where paradoxes correspond to graph cycles and consistent theories relate to digraph kernels. His recent work focuses on the Poison Game for infinite digraphs and a Logic of Sentential Operators (LSO) that handles unrestricted sentential quantification without explosion. His publications span journals such as the Journal of Philosophical Logic, Journal of Symbolic Logic, Synthese, and Discrete Mathematics. He has authored the textbook Introduction to Mathematical Logic and maintains comprehensive lecture notes for courses like INF-227. His work shows a strong trend in using combinatorial and algebraic structures to model logical and computational phenomena, especially in handling inconsistency and self-reference. Strongly complete axiomatizations of finite syntactic epistemic states Complete calculus for multialgebraic semantics of nondeterminism Graph Normal Form for first-order logic Paraconsistent resolution with local kernels Applications of digraph kernels to SAT solving Michal Walicki has supervised several PhD students, including Sjur Dyrkolbotn, Thomas Ågotnes, and Yngve Lamo. He has also received research funding for projects in logic and algebra, though specific grants are not detailed. He leads a research group focused on logical foundations of computation and collaborates with colleagues in logic, computer science, and philosophy. His work continues to explore the deep connections between logic, graphs, and algebraic structures.

Joost-Pieter Katoenمشاهده پروفایل

استاد

• Probabilistic Programming
• Model Checking
• Formal Verification
• +۴ مورد دیگر

Joost-Pieter Katoen is a full professor at RWTH Aachen University in Germany where he leads the Software Modeling and Verification (MOVES) group. Since 2013, he holds a distinguished professorship at RWTH Aachen University and is a member of the Academia Europaea. He also maintains a part-time association with the Formal Methods & Tools group at the University of Twente in the Netherlands. Professor Katoen's research primarily focuses on probabilistic programming, model checking, and formal verification. His work spans theoretical foundations of probabilistic systems, deductive verification techniques for probabilistic programs, and practical applications in software verification. He has made significant contributions to the development of algorithms for analyzing probabilistic models, including Markov chains and probabilistic automata. His research bridges theoretical computer science with practical verification challenges, particularly in the context of probabilistic systems. His recent publications reveal a strong focus on advancing probabilistic programming verification, with particular emphasis on generating functions, expected runtimes, and probabilistic bisimulation. The research trends show increasing sophistication in handling continuous distributions, parameter synthesis, and multi-objective verification problems. His work consistently appears in top-tier conferences including POPL, PLDI, SPLASH, and CAV. Scientific Awards and Recognition: Distinguished Professorship at RWTH Aachen University (since 2013) Member of Academia Europaea Professor Katoen has supervised numerous PhD students whose work spans various aspects of formal methods and probabilistic systems. His MOVES research group develops several verification tools including PROPHESY, PRINSYS, COMPASS, MRMC, and SMYLE. His editorial service includes membership on steering committees for major conferences such as CONCUR and ETAPS (where he serves as chair), and editorial boards for journals including STTT and PeerJ Computer Science.

Véronique Benzakenمشاهده پروفایل

استاد

• Data-Centric Programming Languages
• Formal Verification of Data Management Systems
• XML/JSON Data Processing
• +۳ مورد دیگر

Véronique Benzaken is a Full Professor at Université Paris-Saclay, affiliated with the Laboratoire de Méthodes Formelles (LRI) and INRIA Saclay's Toccata group. Her research focuses on Data-Centric Programming Languages , formal verification of data management systems, and type-safe XML/JSON processing. Key projects: ℂDuce XML-centric functional language, Datacert data certification initiative Collaboration with Oracle Labs on multi-lingual query interfaces using QIR Active in Coq formalization of SQL, Datalog, and data provenance Research interests include: Formal foundations for NoSQL/BigData languages Coq-based verification of database systems Type systems for data models Cloud computing data abstraction Her work bridges theory and practical implementation through collaborations with both academic and industrial partners.

Konstantinos Mamourasمشاهده پروفایل

استادیار

• Programming Languages
• Formal Methods
• Runtime Verification
• +۶ مورد دیگر

Konstantinos Mamouras is an Assistant Professor at the Department of Computer Science, Rice University. His research focuses on programming abstractions for data streams, runtime verification for cyber-physical systems, program semantics, and Kleene Algebra with Tests. Rice University, Houston, TX Department of Computer Science Research Interests : Design of programming abstractions for streaming data Runtime verification of cyber-physical systems Formal methods in program verification Kleene Algebra with Tests (equational theories) Efficient automata-based processing Quantitative monitoring frameworks Recent Scientific Contributions : 2025: Membership Testing for Semantic Regular Expressions (PLDI 2025) 2024: HybridSA GPU regex acceleration (OOPSLA 2024) 2024: Efficient regex with lookaround (POPL 2024) 2023: Bit Vector Automata for regex (OOPSLA 2023) 2021: Quantitative monitoring framework (RV 2021) Scientific Awards : 🏆 Distinguished Paper Award, PLDI 2024 🏆 Best Paper Award, EuroSys 2021 🏆 EATCS Best Theory Paper Award, FoSSaCS 2015 Advising : Mentored PhD student Lingkun Kong (2023) Advised MSc student Zhifu Wang (2022) Current advisees: Alexis Le Glaunec and Agnishom Chattopadhyay Teaching : Spring 2023: IoT Programming and Data Analysis (COMP 418/518) Fall 2022: Reasoning about Algorithms (COMP 382) Spring 2021: Reasoning about Software (COMP 403/503)

Mikołaj Bojańczykمشاهده پروفایل

استاد

• Automata Theory
• Logic in Computer Science
• Monadic Second-Order Logic
• +۷ مورد دیگر

Mikołaj Bojańczyk is a Professor at the Institute of Informatics, Faculty of Mathematics, Informatics and Mechanics, University of Warsaw. He has been affiliated with the University of Warsaw since his undergraduate studies, with brief periods at institutions in Bordeaux and Paris (2004-2005). He received his PhD in 2004 under Igor Walukiewicz, completed his habilitation in 2008, and was promoted to full professor in 2014. Professor Bojańczyk's research lies at the intersection of theoretical computer science and mathematical logic, with a strong emphasis on automata theory. His work spans several interconnected domains: formal language theory, algebraic approaches to language recognition, monadic second-order logic and its extensions, polyregular functions, and the theory of atoms for handling infinite alphabets. He has made significant contributions to understanding the connections between logic and automata for various structures including words, trees, graphs, and data words. His research has particularly focused on characterizing logical definability through algebraic means, developing new automata models for complex structures, and exploring the boundaries of decidability for various logical formalisms. Analysis of his recent publications reveals a continued focus on polyregular functions, MSO transductions, and the theory of atoms. His work demonstrates a consistent pattern of connecting category-theoretic approaches with concrete automata models, often bridging abstract mathematical concepts with practical computational frameworks. A notable trend is his exploration of rank-based approaches in logic and graph theory, as well as deepening connections between algebraic structures and logical definability. Salomaa Prize (2024) PODS Test of Time Award (2016) PODS Best Paper (2013) Presburger Award (2010) Kuratowski Award (2007) Lipski Prize (2006) PODS Best Paper (2006) Ackermann Award (2005) ICALP Best Paper (2004) Professor Bojańczyk has successfully supervised numerous PhD students to completion, including Rafał Stefański (2023), Janusz Schmude (2022), and others dating back to Paweł Parys (2011). He currently supervises four ongoing PhD projects with Kacper Lewandowski, Katzper Michno, Antoni Puch, and Omid Yaghoubi. His grant portfolio demonstrates sustained research leadership, including the current NCN Maestro grant "Polynomial finite-state computation" (2023-2028), previous ERC Consolidator Grant "Lipa" (2016-2021), and ERC Starting Grant "Sosna" (2009-2014). He has also been active in academic service, serving on prestigious committees including the Gödel Prize Committee (2024-2026) and the Presburger Award Committee (2021-2023). Professor Bojańczyk has been instrumental in developing the "atoms" research program at the University of Warsaw, which has its own blog and book. This theoretical framework addresses computation with infinite alphabets through the lens of nominal sets and orbit-finite structures. He has also created educational resources including the "Automata Toolbox" lecture notes and the "Slajdomat" slide software for creating zooming presentations in Figma.

Hossein Hojjatمشاهده پروفایل

استادیار

• Formal Methods
• Software Verification
• Hardware Verification
• +۱۱ مورد دیگر

Hossein Hojjat is an Assistant Professor in the Department of Computer Science at the Rochester Institute of Technology (RIT), within the Golisano College of Computing and Information Sciences. He received his PhD in computer science from EPFL, Switzerland in 2013 and was a postdoctoral researcher at Cornell University before joining RIT. He is currently on leave from his academic position since 2019. Research Interests: His research focuses on formal methods for the analysis and verification of software and hardware systems. He works extensively on program verification, network verification (especially in software-defined networking), automated program repair, Horn clauses, interpolation techniques, and model checking. His work bridges theoretical foundations with practical tools and applications. Publication Trends: His recent publications (2012–2017) show a strong trend in applying formal methods to networked and distributed systems, particularly using NetKAT and Horn clause solvers. He has made significant contributions to ensuring consistency in network updates, synthesizing repairs, and analyzing timed and concurrent systems. His work integrates logic, programming languages, and systems. Scientific Service: Program Committee: FSEN 2015, FSEN 2017, TTCS 2017, VSTTE 2017, SEFM 2017, SBMF 2018, FSEN 2019 (co-chair), PLDI 2019 (AEC) Editorial Board: Information Processing Letters Advising and Grants: He has advised PhD student Ali Shokri and has received research funding through the SaTC: CORE: Small grant on federated network security. His academic advising and grant activities reflect his leadership in advancing formal techniques for secure and reliable systems. Labs and Teams: While no specific lab is mentioned, his collaborations with researchers at EPFL, Cornell, and in tool development (e.g., FLATA, ELDARICA) indicate active participation in formal methods research teams focused on verification toolkits and network programming.

Ohad Kammarمشاهده پروفایل

عضو هیئت علمی

• Programming Language Theory
• Denotational Semantics
• Algebraic Effects
• +۶ مورد دیگر

Ohad Kammar is a Reader at the School of Informatics, University of Edinburgh, where he is affiliated with the Laboratory for Foundations of Computer Science. His research bridges theoretical computer science with practical applications in programming languages, probabilistic computing, and conceptual biology. He holds a Royal Society University Research Fellowship focused on foundations for type-driven data science and is involved in multiple significant research projects including ARIA Safeguarded AI and differentiable probabilistic programming semantics. Dr. Kammar's research spans programming language theory with particular expertise in denotational semantics, algebraic effects, and probabilistic programming. His work explores how to formally model computational effects, create robust type systems, and develop mathematical foundations for probabilistic programming languages. He investigates connections between category theory, domain theory, and practical programming language design, with applications ranging from secure systems to Bayesian inference algorithms. His recent work shows increasing focus on type-driven approaches to data science and AI safety. Kammar's publication record demonstrates consistent high-impact contributions to top-tier programming language conferences (POPL, ICFP, LICS) with notable recognition including the POPL'19 Distinguished Paper Award and the 2025 ISCA Best Paper Award. His work shows a clear trajectory from foundational theory (algebraic effects, denotational semantics) toward practical applications in probabilistic programming and type-driven data science. Recent publications increasingly integrate concepts from category theory, domain theory, and statistical modeling to address challenges in programming language design for modern computing paradigms. 2025 ISCA Best Paper Award for 'Precise exceptions in relaxed architectures' POPL'19 Distinguished Paper Award for 'A Domain Theory for Statistical Probabilistic Programming' Dr. Kammar currently supervises UG4/MInf and MSc projects at the University of Edinburgh and is developing an undergraduate course on type-driven probabilistic modeling. His research is supported by prestigious grants including a Royal Society University Research Fellowship and collaborations with Facebook Research, the National Cyber Security Centre, and the Alan Turing Institute. His work often involves interdisciplinary teams spanning institutions including the University of Oxford, University of Cambridge, and KAIST. He is actively involved with the Laboratory for Foundations of Computer Science and the Bayes Centre at the University of Edinburgh. His recent projects include work with Ehud Lamm's Conceptual Biology Lab, demonstrating his interest in bridging computer science with biological concepts. Dr. Kammar is also known for his community service efforts to liberate academic papers from copyright restrictions, making important historical works in programming language theory more accessible to researchers.

Viktor Kuncakمشاهده پروفایل

دانشیار

• Formal Verification
• Theorem Proving
• Program Synthesis
• +۶ مورد دیگر

Viktor Kuncak is an Associate Professor at the École polytechnique fédérale de Lausanne (EPFL) in the School of Computer and Communication Sciences (IC) , affiliated with the Laboratory for Automated Reasoning and Analysis (LARA) . His work bridges programming languages, formal verification, and automated reasoning. Email: viktor.kuncak@epfl.ch Office: INR 318, EPFL, Lausanne, Switzerland Research Interests: Viktor specializes in formal verification , theorem proving , and program synthesis , focusing on languages, algorithms, and systems for automated reasoning. His research addresses verification of functional programs, constraint solving, and symbolic computation. Recent Publications Trends: His work includes mechanized HOL reasoning, algebraic array theories, interpolation in ortholattices, and symbolic automata complexity. Keywords span automated reasoning, formal methods, and functional programming. Scientific Awards: 2012: 5-year ERC grant (1.5M EUR) ACM SIGSOFT Distinguished Paper Award Invited talks at Lambda Days, Scala Days, and CACM Research Highlights Advising & Grants: Viktor has supervised 15+ PhD students and led a European COST network in automated reasoning. He served as Associate Editor for TOPLAS and co-chaired CAV, FMCAD, and VMCAI conferences. Labs & Teams: He leads LARA , which develops tools like Leon and Stainless for program verification and synthesis. The group focuses on scalable formal methods for reliable software.