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

Asta Halkjær Fromمشاهده پروفایل

پژوهشگر

• Formal Logic
• Automated Reasoning
• Theorem Proving
• +۱۳ مورد دیگر

Asta Halkjær From is a postdoctoral researcher in the Department of Computer Science at the University of Copenhagen, affiliated with the Software, Data, People & Society (SDPS) section under Dmitriy Traytel. She previously completed her PhD at DTU Compute from 2020 to 2023, focusing on formalized deduction methods in computational logic. She holds a Master’s and Bachelor’s degree from DTU in Computer Science and Software Technology, respectively, with a specialization in Artificial Intelligence and Algorithms. Her research lies at the intersection of formal logic and computer science, particularly in automated reasoning, proof assistants (Isabelle/HOL and Lean), and mechanized metatheory. She has contributed extensively to synthetic completeness proofs, tableau systems, and verified theorem provers. Her work emphasizes formal verification of logical systems, including epistemic logic, hybrid logic, and first-order logic, with a focus on soundness and completeness. The recent publications highlight a consistent trend: the mechanization of logical foundations in proof assistants. Her work bridges theoretical logic with practical verification tools, enabling reliable automation in theorem proving. She has developed and verified provers, explored axiomatic systems, and advanced the methodology of synthetic completeness, often leveraging Isabelle/HOL’s framework. Distinguished Paper Award, CPP 2023 DTU Young Researcher Award DTU Travel Grant (Executive Board Recognition) Otto Mønsted Fonden Travel Grant She has supervised BSc and MSc theses, special courses, and research projects at DTU, and currently teaches Software Development for Digital Health . She has served on program committees for CPP, ITP, and Dalí workshops and has reviewed for journals including Journal of Automated Reasoning and Journal of Logic and Computation . She has also participated in international research visits, including at VU Amsterdam. She is actively involved in building tools for formal reasoning and maintains a personal website with resources, including an Isabelle snippets generator and bibliography tools. Her work continues to advance the foundations of formal logic through mechanized proofs and practical automation.

Alexander Steenمشاهده پروفایل

استادیار

• Computational Logic
• Automated Reasoning
• Theoretical Computer Science
• +۷ مورد دیگر

Alexander Steen is an Assistant Professor (Juniorprofessor) at the University of Greifswald within the Institute of Mathematics and Computer Science. His research focuses on computational logic, automated reasoning, and theoretical computer science, with significant contributions to higher-order logic (HOL) and non-classical reasoning systems. He leads the development of the Leo-III automated theorem prover, a versatile system supporting classical HOL with choice, polymorphic logics, and higher-order modal/deontic logics. Steen's academic journey includes a Dr. rer. nat. (summa cum laude) from Freie Universität Berlin (2018), followed by post-doctoral work at the University of Luxembourg (2018-2021) as a principal investigator for the AuReLeE project on legal reasoning automation. He holds a 2024 nomination for the University of Greifswald Teaching Award and was elected Fellow of the Academy of Sciences and Humanities in Hamburg (2022). Key Research Areas: Higher-Order Logic, Automated Reasoning, Non-Classical Logics, Legal Tech, Formal Methods in AI, Computational Ethics. Major Projects: Leo-III (DFG-funded automated prover), AuReLeE (FNR-funded legal reasoning), MET (modal logic embedding tool). His recent publications (2025-2022) explore diverse applications of HOL in non-classical reasoning, legal formalization, argumentation frameworks, and TPTP infrastructure extensions. Steen actively contributes to AI governance as co-speaker of the GI AI section and deputy member of Greifswald's Senate. He also engages in science communication through works like the 2024 science comic book Was wissen wir schon (What Do We Know?), featuring his automated reasoning research. Scientific Honors: CLAR 2023 Best Paper Award, IRIS 2020 LexisNexis Best Paper Award, CASC-27 LTB Division Winner, Woody Bledsoe Travel Awards (CADE 2018, 2016), GI Junior Fellowship (2018). Advising: Supervises ongoing PhD/MSc/BSc theses in logic-based AI, modal reasoning, and legal tech at University of Greifswald and Freie Universität Berlin.

Talia Ringerمشاهده پروفایل

استادیار

• Verification
• Proof Engineering
• Dependent Type Theory
• +۳ مورد دیگر

Talia Ringer is an Assistant Professor at the University of Illinois at Urbana-Champaign , focusing on making program verification using interactive theorem provers more accessible through improved proof engineering tools and practices. Her research addresses challenges in maintaining proofs as programs evolve and advancing formal verification. Ph.D., University of Washington (2021), NSF GRFP and P.E.O. Fellow B.S., Mathematics and Computer Science, University of Maryland Former software engineer at Amazon Her research interests include: Program Verification Proof Engineering Dependent Type Theory Interactive Theorem Provers (Coq) Key trends in her publications include: Automated proof generation and repair using large language models Tool development for Coq and other proof assistants Formal verification of software and data structures Integration of identifiers and type equivalences in verification Test input generation for software reliability Scientific awards and honors: NSF Graduate Research Fellowship Program (GRFP) P.E.O. Scholar Award She has advised numerous researchers through her work and founded the SIGPLAN-M Mentoring Program and Computing Connections Fellowship . No specific student names are listed in the scraped text.

Carlo Angiuliمشاهده پروفایل

استادیار

• Type Theory
• Programming Language Foundations
• Homotopy Type Theory
• +۳ مورد دیگر

Carlo Angiuli is an Assistant Professor of Computer Science at the Luddy School of Indiana University . He is a leading researcher in type theory , with a focus on its applications to programming language design and logic . His work bridges theoretical foundations and practical implementations, particularly through dependent types , proof assistants , and homotopy type theory . His research interests include: Type Theory (foundational systems for programs and proofs) Programming Language Foundations (formal semantics and reasoning) Homotopy Type Theory (higher-dimensional structures) Dependent Types (expressive type systems) Proof Assistants (formal verification tools) Computational Logic (algorithmic reasoning) Angiuli actively contributes to the programming languages community as a POPL Program Committee member and co-author of a forthcoming textbook on dependent type theory. His students include Johnson He, Huang Xu, Kelton OBrien, and Ian Ray , who joined in Fall 2025. He has received significant recognition, including the Best Paper Award at FSCD 2019 and the School of Computer Science Distinguished Dissertation Award from Carnegie Mellon University. His current work explores advanced type-theoretic frameworks and their implementation in proof assistants like the red* family of tools. Scientific awards: Best Paper Award, FSCD 2019 (Junior Researchers category) School of Computer Science Distinguished Dissertation Award, Carnegie Mellon University He teaches courses such as Modern Dependent Types (CSCI-B619), Programming Language Foundations (CSCI-B522), and Introduction to Computer Science (CSCI-C211).

• Theoretical Computer Science
• Theorem Proving
• Automated Reasoning
• +۲۶ مورد دیگر

Jasmin Blanchette is a Professor of Theoretical Computer Science and Theorem Proving at Ludwig-Maximilians-Universität München (LMU), where he also serves as the Dean of Studies for Computer Science since January 22, 2024. He is affiliated with the Institute for Informatics and leads the Theoretische Informatik und Theorembeweisen research unit. Additionally, he is a guest researcher in the VeriDis group at Loria, Nancy. Research Interests: His research centers on strengthening proof automation for general-purpose logics and enhancing the usability of proof assistants. He combines automatic and interactive methods, bridging human and artificial intelligence in formal verification. His work spans higher-order logic, automated and interactive theorem proving, formalization of mathematical results, and foundational mechanisms for (co)datatypes and (co)recursive functions. Key projects include Sledgehammer, Nitpick, Matryoshka, Nekoka, IsaFoL, and Lean Forward. Publication Trends: His recent publications (2023–2025) show a strong focus on higher-order automated reasoning, superposition calculus, proof automation in Isabelle/HOL, and formalization of logical and mathematical concepts. There is a consistent emphasis on verification, efficiency, and integration of SAT/SMT techniques into higher-order provers. Scientific Awards: FroCoS 2023 Best Paper Award (with Visa Nummelin and Sander Dahmen) CADE 2023 Best Paper Award for 'Verified given clause procedures' (with Qi Qiu and Sophie Tourret) IPA Dissertation Award (awarded to student Petar Vukmirović) Dutch Prize for ICT Research 2022 Advising and Grants: He supervises a large team of postdocs and PhD students at LMU and co-supervises students at other institutions. His leadership in major collaborative projects like Matryoshka indicates significant grant funding and collaborative research efforts. He is editor-in-chief of the Journal of Automated Reasoning and serves on numerous steering and program committees, reflecting strong academic leadership and visibility. Labs and Teams: He leads a research group at LMU’s Institute for Informatics, focusing on theorem proving and formal methods. He is also associated with the VeriDis group at Loria, Nancy, and collaborates widely across Europe in the automated reasoning community.

Claudia Schonمشاهده پروفایل

پژوهشگر

• Automated Reasoning
• Artificial Intelligence
• Knowledge Representation
• +۳ مورد دیگر

Claudia Schon is a Researcher at the Institute of Computer Science, Department 4, University of Koblenz-Landau. Her work focuses on automated reasoning, cognitive systems, and knowledge representation. She has contributed to projects like the Corg Project, exploring cognitive reasoning mechanisms and integrating commonsense knowledge into automated theorem provers. Her research bridges logic-based AI with human reasoning models, addressing challenges in uncertainty management, associative reasoning, and deontic logic. Key areas of research include commonsense reasoning, deductive systems, and the application of large language models to knowledge selection. She has published extensively on topics such as negation in cognitive reasoning, concept contraction in description logics, and intentional forgetting in AI systems. Her work often emphasizes interdisciplinary approaches, combining formal logic with cognitive science and philosophy. Her publications from 2019 to 2024 reflect a steady focus on advancing automated reasoning methodologies, integrating human-like cognitive processes into AI systems. Recent work explores the next generation of deduction systems and the use of word embeddings for axiom selection. She has also contributed to workshops on linguistic and cognitive approaches to dialog agents, highlighting her interest in human-AI collaboration. Despite no listed scientific awards, her contributions are recognized through active publication in top-tier conferences and journals. She is affiliated with the E-KRHyper project, developing reasoning tools for description logics. Her advising roles and grants are not explicitly documented in the provided text.

Julie Caillerمشاهده پروفایل

دانشیار

• Automated Deduction
• Theoretical Computer Science
• Formal Methods
• +۶ مورد دیگر

Julie Cailler is an Associate Professor at the University of Lorraine, affiliated with CNRS, Inria, and LORIA in Nancy, France. She is a member of the VeriDis Team and focuses on automated deduction, interactive proof systems, and logic in computer science. PhD in Theoretical Computer Science from the University of Montpellier (2023) Former Associate Professor at the University of Regensburg Her research interests include: Designing concurrent and parallel decision procedures for first-order logic Integration of automated and interactive theorem proving Proof system interoperability and formal verification Recent publications highlight her work on: SC-TPTP format extensions for sequent-based proofs (CADE-30, 2025) Graph Neural Networks for word equation solving (ATVA 2024, 2025) Deskolemization strategies in first-order logic (LPAR 25, 2024) Scientific recognition: Woody Bledsoe Award (2022) Best Newcomer Prover (CASCJ11, 2022) She supervises students in projects related to: Automated theorem prover development Logic programming and deduction modulo theory Formal verification and proof tool integration Julie is actively involved in academic service as: Co-head of GT LVP (Languages and Program Verification) working group PC member for major conferences like FMCAD, FSTTCS, and ITP

Paige Randall Northمشاهده پروفایل

استادیار

• Category Theory
• Homotopy Theory
• Functional Programming
• +۳ مورد دیگر

Paige Randall North is an Assistant Professor at Utrecht University, holding dual appointments in Mathematics and Information and Computing Sciences. She is also an Honorary Research Fellow at the University of Birmingham and a Guest Researcher at Delft University of Technology. Her research focuses on applying category theory and topology to computer science, particularly in functional programming and homotopy theory. North earned her PhD in Mathematics from the University of Cambridge (supervised by Martin Hyland) and a BS from the University of Chicago. She has held postdoctoral positions at the University of Pennsylvania and Ohio State University. Her research explores connections between type theory and higher category theory, including the univalence principle and categorical diffusion. Recent activities include organizing conferences like TYPES and DutchCATS, serving on program committees for LICS and POPL, and teaching advanced courses on homotopy type theory and interactive theorem provers. Funding has come from the AFOSR (2021-2024). Her work emphasizes formalization in proof assistants like UniMath and Coq, with contributions to categorical semantics and bicategorical type theory.

Alastair F. Donaldsonمشاهده پروفایل

استاد

• Programming Languages
• Compilers
• Verification
• +۲ مورد دیگر

Alastair F. Donaldson is a Professor in the Department of Computing at Imperial College London's Faculty of Engineering, where he leads the Multicore Programming Group. He also works as a Software Engineer at Google in the Android Graphics Team. Previously, he served as Director of GraphicsFuzz, an Imperial College spinout company acquired by Google in 2018. His research spans programming languages, compilers, verification, and testing, with a particular focus on randomized and fuzz testing techniques for compilers and program analyzers. Donaldson has developed several influential testing frameworks including GraphicsFuzz, RustSmith, and GrayC, which have significantly advanced compiler testing methodologies. Analysis of his recent publications reveals a strong trend toward practical applications of compiler testing techniques across diverse domains including GPU programming, verification-aware languages, and memory models. His work increasingly incorporates continuous integration practices and focuses on addressing real-world challenges in compiler development and verification. Donaldson maintains active involvement in the programming languages research community, serving on program committees for major conferences including PLDI, POPL, ASPLOS, and SPLASH. He has contributed significantly to advancing compiler testing methodologies and has mentored numerous researchers through PLMW (Programming Languages Mentoring Workshop). He leads the Multicore Programming Group at Imperial College London, which focuses on challenges in parallel and concurrent programming. His work bridges theoretical computer science with practical software engineering challenges, particularly in the areas of compiler correctness and verification.

Michael H. Borkowskiمشاهده پروفایل

استاد آموزشی

• Software Verification
• Type Theory
• Interactive Theorem Provers
• +۳ مورد دیگر

Michael H. Borkowski is an Assistant Teaching Professor in the Department of Computer Science at Purdue University. He earned his Ph.D. from the University of California, San Diego (UCSD), specializing in software verification, type theory, and interactive theorem provers. His research focuses on developing techniques to ensure software correctness and performance through formal methods. Ph.D., UCSD Computer Science (2024) M.S., UCSD Computer Science (2019) B.A., Amherst College Computer Science (2016) His research interests include refinement types, functional programming, and mechanizing proofs. Recent work emphasizes software verification tools (e.g., the 2024 POPL publication on refinement types). Earlier contributions span plant biology and applied mathematics, including studies on auxin gradients and wood grain modeling. Notable awards include the Computer Science Prize and Phi Beta Kappa from Amherst College. Teaching roles include courses at UCSD (e.g., CSE 20 Discrete Mathematics) and Purdue. He was affiliated with UCSD’s ProgSys Group during his Ph.D.

Louis Salvailمشاهده پروفایل

استاد

• Quantum Computing
• Cryptography
• Quantum Cryptography
• +۴ مورد دیگر

Louis Salvail is a Full Professor at the University of Montréal’s Department of Computer Science and Operations Research, affiliated with the Laboratory for Theoretical and Quantum Computing (LITQ). He joined the university in 2008 after working at Aarhus University from 1998 to 2008, where he contributed to classical cryptography foundations. His primary research interests are quantum-classical cryptography and quantum information theory, with a focus on theoretical problems. He teaches courses like Cryptology and Quantum Computing. Research projects include leadership on quantum cryptography protocols and collaborations in quantum networks. Notable grants include those from NSERC (Canada) and FQRNT, focusing on quantum cryptography foundations and quantum communication technologies. He has advised numerous PhD and Master’s students on topics like quantum key distribution protocols and cryptographic security. Salvail holds a 1998 PhD from Université de Montréal under Gilles Brassard and Claude Crépeau.

Hongjin Liangمشاهده پروفایل

دانشیار

• Programming Languages
• Formal Verification
• Concurrency Theory
• +۳ مورد دیگر

Hongjin Liang is an Associate Professor at the School of Computer Science , Nanjing University , China. He is an active researcher and educator in the fields of programming languages and formal verification, with a strong focus on concurrency theory, mechanized proofs, and memory models. Education: PhD in Computer Science (May 2014), dissertation titled Refinement Verification of Concurrent Programs and Its Applications . Research Interests: His research spans formal verification , concurrent programming , memory models , and mechanized reasoning . He is particularly known for his work on verifying concurrent data structures, program logics for concurrency, and certified compilation. He is a member of the PLaX research group . Publications and Impact: Liang has published extensively in top-tier venues such as POPL, PLDI, ESOP, TOPLAS, and CSL-LICS. His work often involves formalizing and verifying complex concurrent systems using interactive theorem provers like Rocq/Coq. Notable contributions include verifying compiler optimizations under weak memory models and developing program logics for randomized concurrent programs. Scientific Awards: Distinguished Paper Award , PLDI 2019 for "Towards Certified Separate Compilation for Concurrent Programs" Teaching and Advising: He teaches undergraduate and graduate courses including Formal Semantics of Programming Languages , Concurrency: Algorithms and Theories , and Compiler Design . He has supervised graduate students and served on numerous program committees for international conferences. Affiliations: He is affiliated with the PLaX research group at Nanjing University and has collaborated with researchers such as Xinyu Feng, Zhong Shao, and Jan Hoffmann.

A.E. Zaidmanمشاهده پروفایل

استاد

• Software Testing
• Test Amplification
• Mutation Testing
• +۶ مورد دیگر

A.E. Zaidman is a Professor in the Software Technology department at Delft University of Technology's Faculty of Electrical Engineering, Mathematics and Computer Science. His research focuses on software testing, code quality, and developer tooling, with recent emphasis on socio-technical factors, environmental impacts of testing, and GitHub Actions workflows. Key Research Areas Test amplification (developer interactions with automated testing) Code smell detection and its impact on software quality Empirical studies in open-source software testing AI/ML applications in test generation and analysis Scientific Awards Best Artifact Award (2022) Best Emerging Results Paper Award (2018) Best ERA paper award (2015) Best tool demo paper award (2017) ICPC 2009 Best Paper Award Recent Publications 2025: Systematic mapping of qualitative software testing methods 2025: Industrial language engineering case studies using Spoofax 2024: Environmental impact analysis of Java testing 2024: GitHub Actions workflow smell investigations

Albert Qiaochu Jiangمشاهده پروفایل

پژوهشگر ارشد

• Machine Learning
• Theorem Proving
• Artificial Intelligence
• +۳ مورد دیگر

Albert Qiaochu Jiang serves as a Visiting Research Fellow at the Department of Computer Science and Technology, University of Cambridge. His research integrates machine learning with formal theorem proving, focusing on neural theorem provers and mathematical reasoning systems. He leads the reasoning team at Mistral AI while maintaining academic supervision at Cambridge. His research interests center on machine learning for theorem proving , with specific expertise in neural-symbolic integration, autoformalization, and large language models for mathematical reasoning. His work bridges artificial intelligence with formal verification, developing systems that enhance automated reasoning capabilities through neural networks. Current projects involve improving premise selection for theorem provers, multilingual mathematical formalization, and creating efficient architectures for mathematical language models. Analysis of his recent publications reveals a strong focus on advancing neural theorem proving through innovative architectures like Target-Based Automated Conjecturing and Magistral. His research trajectory shows increasing sophistication in integrating language models with formal verification systems, with significant contributions to datasets like Numinamath and frameworks like Llemma. Key trends include optimizing compute efficiency in proof generation, enhancing multilingual mathematical reasoning, and developing interactive human-AI collaboration systems for formal mathematics. While no scientific awards are currently documented in available sources, his research output demonstrates significant impact in the intersection of AI and formal methods. As leader of Mistral AI's reasoning team, Jiang directs research on neural theorem proving systems while contributing to academic supervision at Cambridge. His work involves substantial industrial-academic collaboration, leveraging resources from both institutional contexts to advance mathematical AI. Current projects focus on creating practical systems for mathematical automation with real-world verification applications. His research operates at the intersection of academia and industry through Mistral AI's reasoning team, where he develops neural theorem proving systems with practical applications in formal verification. This dual affiliation enables rapid translation of theoretical advances into deployable tools for mathematical automation.

Alexander R. Blockمشاهده پروفایل

استادیار

• Cryptography
• Coding Theory
• SNARKs
• +۷ مورد دیگر

Dr. Alexander R. Block is an Assistant Professor at the University of Illinois at Chicago (UIC) , specializing in Cryptography and Coding Theory . He focuses on the concrete security and space-efficiency of SNARKs, error-correcting codes , and locally decodable codes . Before UIC, he was a postdoctoral researcher at Georgetown University and University of Maryland , advised by Justin Thaler and Jonathan Katz. His PhD from Purdue University (2022) was supervised by Jeremiah Blocki. His research bridges theoretical and applied aspects, including field-agnostic SNARKs (CRYPTO 2024) with expand-accumulate codes, Fiat-Shamir security analysis of FRI protocols (ASIACRYPT 2023), and memory-hard puzzles in the standard model (SCN 2022). He has contributed to insertion-deletion error codes (CCC 2023) and secure computation with leaky correlations (TCC 2018, CRYPTO 2017). Dr. Block has received multiple scientific awards , including the Emil Stefanov Fellowship (2021) and Purdue Three Minute Thesis Competition Finalist (2022). His teaching includes courses like UIC's CS 505 - Computability and Complexity Theory (Spring 2025), where he emphasizes interactive proofs and zero-knowledge systems . He actively serves on program committees for CRYPTO , EUROCRYPT , and ZKProof Workshop , and has reviewed for leading journals and conferences.