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

Peter Dybjerمشاهده پروفایل

استاد

• Intuitionistic Type Theory
• Categorical Type Theory
• Proof Assistants
• +۹ مورد دیگر

Peter Dybjer is a Professor of Computing Science at the Department of Computer Science and Engineering, Chalmers University of Technology in Sweden. He is a leading researcher in the field of type theory, with a focus on intuitionistic type theory, categorical semantics, and proof assistants. His work bridges foundational aspects of mathematics and computer science, emphasizing constructive methods and formal verification. Research Interests: Intuitionistic Type Theory and its categorical semantics Proof assistants and formal verification Inductive and inductive-recursive definitions Game semantics and normalization techniques Dependent type systems and their applications Homotopy Type Theory and univalent foundations Activities & Contributions: Editor of the Bulletin of Symbolic Logic Member of program committees for conferences like TYPES, FSCD, and MFPS Keynote speaker at events including the European Congress of Mathematics and the Hausdorff Research Institute's Summer School on Types, Sets, and Constructions Initiated and directed the Master's Program in Computer Science – Algorithms, Languages, and Logic at Chalmers Teaching & Outreach: Professor Dybjer has taught advanced courses at international summer schools, including: Inductive Definitions in Constructive Type Theory (TYPES Summer School, 2005) Dependent Types at Work (LerNet Summer School, Uruguay, 2008) Normalization by Evaluation (Midlands Graduate School, 2009 and 2015)

Tiark Rompfمشاهده پروفایل

استادیار

• Compiler Design
• Programming Languages
• Runtime Code Generation
• +۸ مورد دیگر

Tiark Rompf is an Assistant Professor at Purdue University , with research spanning programming languages, compilers, and systems. His work bridges domains including architecture, databases, machine learning, and AI through projects like Reachability Types and Rhyme. Co-director of the Purdue Center for Programming Principles and Software Systems (PurPL) Scientific Advisor at SambaNova Systems Previously a member of the Scala team at EPFL His research focuses on: Runtime code generation and advanced compiler technology Expressive data-centric query languages (Rhyme, Datalog) Reachability type systems for memory safety and effect handling Metaprogramming and logical relations for formal verification Recent publications highlight contributions to Datalog compilation (Flan), nested data structures (Rhyme), and polymorphic reachability types. He leads projects exploring: Compiler optimizations for emerging architectures (GPU, TPU, FPGA) ML-driven compiler improvements Secure multi-party computation via metaprogramming Scientific awards include: NSF CAREER Award (2016) Google Faculty Research Awards (2017, 2018) DOE Early Career Research Award (2017) ACM SIGPLAN PL Software Award (2019) GPCE Test of Time Award (2020) Students and alumni from his group have joined institutions like Databricks, DeepMind, Galois, and Meta. He teaches advanced compiler courses including: CS 590 - Advanced Topics in Compilers CS 352 - Compilers CS 502 - Graduate Compilers

Fredrik Kjolstadمشاهده پروفایل

استادیار

• Compilers
• Programming Models
• Systems
• +۵ مورد دیگر

Fredrik Kjolstad is an Assistant Professor of Computer Science at Stanford University. His research focuses on compilers, programming models, and systems for sparse computing, with an emphasis on separating algorithms from data representation. He leads efforts in developing compilers like TACO, Simit, and Legate Sparse to optimize sparse tensor algebra and distributed computations. Kjolstad's work spans compiler design, hardware-software co-design, and programming languages for high-performance computing. His research group aims to enable portable applications across diverse data representations and architectures. Notable projects include the TACO compiler for sparse tensor algebra, the Simit programming language for physical simulations, and the Copy-and-Patch compilation technique for fast runtime code generation. He has also contributed to distributed systems like Legate Sparse and hardware accelerators such as Onyx. Kjolstad has received prestigious awards including the NSF CAREER Award and the MIT EECS PhD Thesis Award. His publications cover topics like sparse tensor compilation, compiler optimization, and agile hardware design. He advises multiple PhD students and collaborates with researchers like Kunle Olukotun and Alex Aiken. Key areas of impact include efficient sparse data processing, compiler-driven hardware design, and scalable distributed computing frameworks. His work bridges theoretical compiler techniques with practical system implementations, aiming to simplify and accelerate complex computational tasks.

Michael Raskinمشاهده پروفایل

مدرس

• Theoretical Computer Science
• Distributed Systems
• Algorithms
• +۶ مورد دیگر

Michael Raskin is a Lecturer (maître de conferences) at LaBRI, University of Bordeaux, where he conducts research in theoretical computer science with a focus on distributed systems and formal methods. His work bridges theoretical foundations with practical implementations, particularly in population protocols, temporal graphs, and Petri nets. His research interests span Theoretical Computer Science , Distributed Systems , Algorithms , and Formal Methods , with specific expertise in population protocols, temporal graph analysis, vector addition systems, and verification techniques for parameterized systems. His publications demonstrate a consistent focus on computational complexity, state complexity, and threshold phenomena in distributed models. Recent publication trends show a strong emphasis on temporal graph theory (with multiple papers on random temporal graphs and giant components), population protocol analysis (including modular protocols and leaderless rendez-vous systems), and verification techniques for parameterized systems. His work often combines mathematical rigor with practical implementation insights. Raskin has developed significant software projects including: Agnostic Lizard - A portable code walker for Common Lisp QueryFS - A filesystem defined through compiled queries His technical contributions span both theoretical advances and practical systems implementation, with a recurring theme of applying programming language techniques to systems problems. His work on Common Lisp tools demonstrates a commitment to practical language implementation alongside theoretical research.

Stephanie Weirichمشاهده پروفایل

استاد

• Programming Languages
• Dependent Types
• Type Systems
• +۳ مورد دیگر

Stephanie Weirich is the ENIAC President's Distinguished Professor in the Department of Computer and Information Science at the University of Pennsylvania's School of Engineering and Applied Science. Her research focuses on programming languages, with emphasis on dependent types, formal verification, and functional programming semantics. She leads Penn's Programming Languages Group (PLClub) and teaches courses including Advanced Programming (CIS 5520) and Programming Languages and Techniques (CIS 120). Research Areas: Her work spans theoretical foundations and practical implementations, including type systems for security, mechanized program verification, cost analysis for lazy evaluation, and language-based techniques for probabilistic programming. Recent projects explore indistinguishability in dependent types and effects systems for resource-aware computation. Honors: SIGPLAN Robin Milner Young Researcher Award (2016) NSF CAREER Award (2004) Microsoft Outstanding Collaborator (2016) Most Influential Paper Award, ICFP (2016) DARPA Computer Science Study Panel (2007-2008) Advising: Mentored 15+ PhD graduates including Richard Eisenberg (2016 Reynolds Award winner) and Vilhelm Sjöberg. Current students work on stratified type theory and mechanized logical relations. Secured grants from NSF and DARPA for research in dependently typed systems. Collaborations: Leads the PLClub research group; collaborates with industry (Microsoft) on Haskell extensions and verification tools like Hs-to-Coq.

• Software Engineering
• Model-Driven Engineering
• Digital Twins
• +۳ مورد دیگر

Antoine Beugnard is a Professor in the Computer Science Department at IMT Atlantique. He received his PhD in Computer Science from the University of Rennes 1 (1993) and accreditation to supervise research in 2005. His career spans academia and industry, including roles at ENST-Bretagne, Telecom Bretagne (now IMT Atlantique), and Michael Jackson France. Education: PhD in Computer Science (University of Rennes 1, 1993), Accreditation to Supervise Research (2005) Affiliation: IMT Atlantique, Lab-STICC (UMR 6285), P4S team Beugnard's research focuses on software modeling, particularly digital twins, model federation (via Openflexo/FML), and late-binding semantics in heterogeneous object-oriented languages. He explores interoperability challenges in multi-language systems and advocates for unified semantics to improve component compatibility. Key trends in his publications include model-driven engineering, digital twin architectures, and formal modeling notations. His work bridges theoretical foundations with industrial applications, notably in telecom systems for Orange and multi-level modeling frameworks. Advising and grants highlight his mentorship of 10+ PhD candidates and leadership in projects like Openflexo. He actively contributes to academic discussions on modeling methodologies and software development processes.

Chris Hawblitzelمشاهده پروفایل

پژوهشگر

• Programming Languages
• Operating Systems
• Verification
• +۴ مورد دیگر

Chris Hawblitzel is a Senior Principal Researcher at Microsoft Research , affiliated with the Systems Research Group – Redmond . His work bridges programming languages, operating systems, verification, and security, emphasizing the integration of safe programming language features into systems development. Research interests include: Programming Languages and Type Systems Formal Verification of Systems Software Language Design for Security and Safety Systems and Networking Recent publications highlight advancements in Rust verification, linear types for systems, proof automation in F*, assembly language verification, and tactic languages. Key trends involve leveraging type systems for safety, SMT-based automation, and cross-layer formal methods. He has contributed to academic communities as a committee member for conferences such as PLDI 2025 , OOPSLA 2023 , and CPP 2019 , alongside session chair roles.

Roopsha Samantaمشاهده پروفایل

استادیار

• Program synthesis
• Program repair
• Concurrency
• +۳ مورد دیگر

Roopsha Samanta is an Assistant Professor in the Department of Computer Science at Purdue University, where she leads the Purdue Formal Methods (PurForM) research group and is a core member of the Purdue Programming Languages (PurPL) group. She completed her PhD at the University of Texas at Austin in 2013 under the supervision of E. Allen Emerson and Vijay K. Garg, followed by postdoctoral research at IST Austria (2014-2016) with Thomas A. Henzinger. Her research focuses on developing foundational techniques at the intersection of formal methods and programming languages, with primary interests in: Program synthesis and repair using semantic guidance Modular verification of distributed systems Concurrency and synchronization synthesis Robustness analysis of I/O systems Her publication record shows consistent contributions across programming languages and formal methods venues, with recent emphasis on explainable program synthesis, bounded verification of distributed systems, and semantics-guided approaches to enhance synthesis robustness. Her work frequently appears in premier conferences including PLDI, POPL, OOPSLA, and CAV. Notable scientific recognitions include: NSF CAREER Award (2019) Amazon Research Award (2021) She actively advises graduate and undergraduate researchers in the PurForM group, with current students including Nouraldin Jaber, Christopher Wagner, and Yongwei Yuan. Her research is supported by grants from NSF and Amazon. Beyond research, she teaches courses on program reasoning (CS560) and neurosymbolic program synthesis (CS592), and serves on steering committees for VMW@CAV and DARS. She also co-edits the ACM SIGPLAN Blog on PL Perspectives.

Daniel Y Chenمشاهده پروفایل

مدرس

• Data Science Education
• Statistics
• Bioinformatics
• +۳ مورد دیگر

Daniel Y Chen is a Lecturer in the Department of Statistics at the University of British Columbia (UBC), Vancouver Campus. He holds a PhD Candidate status in Genetics, Bioinformatics, and Computational Biology at Virginia Tech, focusing on data science education in the biomedical sciences. His expertise includes statistical computing, open source software development, and reproducible research practices. Education: PhD Candidate (in progress): Genetics, Bioinformatics & Computational Biology, Virginia Tech MSc: Relevant field (implied via career progression) Research Interests: Daniel's work bridges data science pedagogy and biomedical applications. He focuses on improving computational literacy among medical practitioners through accessible education resources, open source tools, and reproducible workflows. His technical contributions span R and Python ecosystems, including packages like grader and pyprojroot , and authoring Pandas for Everyone . He actively promotes best practices in scientific programming and collaborative software development. Grants & Contributions: Contributions to RStudio's gradethis and learnr packages Open source maintenance (e.g., Arch Linux AUR packages) Labs/Teams: Affiliated with UBC's Data Science for Biomedicine (DS4BIOMED) initiative and Virginia Tech's Social Decision Analytics Laboratory. Collaborates with RStudio and GitHub communities on education and tool development.

• Programming Languages
• Type Theory
• Compiler Construction
• +۴ مورد دیگر

Björn Lötters, M.Sc., is a Lecturer and research associate at the Technical University of Central Hesse (THM) within the Department of Mathematics, Natural Sciences and Computer Science. He is also a doctoral student in collaboration with the Justus Liebig University. His primary teaching responsibilities include courses on functional programming, compiler construction, and programming language design, with a focus on empowering students to explore advanced topics like dependent types and syntax abstraction. Education: Studied computer science at THM until 2019. Career: Worked as a software engineer until 2021, then transitioned to academia as a research associate and lecturer at THM. Research Focus: Programming languages (design & implementation) Type systems and type theory Metaprogramming tools Software architecture and design His ongoing research projects include a doctoral thesis on the application of intuitionistic type theory in programming languages and a study on syntax abstraction mechanisms. He actively supervises bachelor's and master's theses, offering topics related to dependent type elaborators, reference management systems, and educational LISP platforms.

• Programming Languages
• Formal Verification
• Functional Programming
• +۹ مورد دیگر

Li-yao Xia is a researcher at INRIA Saclay in France, with a focus on programming languages, formal verification, and functional programming. His research explores bidirectional programming, lazy evaluation, concurrency, and mechanized verification using tools like Coq and Haskell. His work spans conferences such as ICFP, POPL, and SPLASH, where he has authored and co-authored papers on topics including interaction trees, transactional objects, and demand semantics for cost analysis. He has also served on program committees for Haskell and HIW. For more details, visit his personal website: https://poisson.chat .

Nada Aminمشاهده پروفایل

استادیار

• Programming Languages
• Artificial Intelligence
• Metaprogramming
• +۴ مورد دیگر

Nada Amin is an Assistant Professor of Computer Science at Harvard University's John A. Paulson School of Engineering and Applied Sciences (SEAS), where she leads the metareflection lab . Her research combines programming languages (PL) and artificial intelligence (AI), focusing on neuro-symbolic systems that are correct by construction, with applications in program synthesis, verification, and precision medicine. Harvard John A. Paulson School of Engineering and Applied Sciences (2019–Present) University Lecturer in Programming Languages at University of Cambridge (2017–2019) Doctoral and postdoctoral work at EPFL (2011–2017) Her research spans three core themes: Safer : Type systems and formal verification (Coq, Dafny, Frama-C) Faster : Multi-stage programming and interpreter collapsing techniques Easier : Neuro-symbolic AI for program manipulation and biological reasoning Key publications include: 2025: Modular Imperative with LLMs (LMPL), Multi-stage Relational Programming (PLDI) 2024: Persimmon for extensible variant types (OOPSLA) 2023: LURK for recursive knowledge (ICFP), Dolorem language growth pattern (ECOOP) Scientific honors include: Teaching Assistant Team Award (EPFL, 2015) Michigan Cambridge Research Initiative Grant (2018) ArsDigita Prize (1999) She has served on program committees for GPCE (co-chair), ICFP, PLDI, and organized workshops in metaprogramming and logic programming. Her teaching portfolio includes graduate courses on neurosymbolic programming, program synthesis, and advanced PL theory.

Andreas Abelمشاهده پروفایل

مدرس ارشد

• Type Theory
• Dependent Types
• Programming Languages
• +۷ مورد دیگر

Andreas Abel is a Senior Lecturer in the Department of Computer Science and Engineering at Gothenburg University, with additional affiliation at Chalmers University of Technology. He is a senior developer of the Agda programming language and maintains the Backus Naur Form Compiler (BNFC). His educational background includes a Computer Science diploma (1999), PhD (2006), and Habilitation (2013), all from Ludwig-Maximilians-University (LMU) Munich. His career spans positions at LMU, INRIA Paris, and Chalmers before his current role at Gothenburg University since 2013. Abel's research focuses on dependently typed programming , type theory , and verified software development . His work bridges theoretical foundations with practical implementations, particularly in the Agda proof assistant. His interests span from foundational aspects of lambda calculus and normalization to practical applications in programming language design. His publications demonstrate a consistent focus on type theory foundations and practical implementations, with recent work exploring applicative functors, cubical type theory, modalities in type systems, and formalizations of algebraic structures. His research often combines deep theoretical insights with concrete implementations in proof assistants. Distinguished Paper Award at ICFP 2019 (4 out of 39 accepted papers) Editor of Theoretical Pearls column, Journal of Functional Programming Member of IFIP WG 1.3 on Foundations of System Specification Abel actively supervises students through the Initial Types Club and Master's thesis projects, focusing on advanced topics in programming languages and type theory. He teaches Programming Language Technology and Advanced Functional Programming, emphasizing both theoretical foundations and practical implementation. His current research is supported by a Vetenskapsrådet grant for the project 'Modal Dependent Type Theory' (2020-2024), continuing his long-standing contributions to programming language theory and formal verification.

• Programming Languages
• Static Analysis
• Software Engineering
• +۷ مورد دیگر

Qirun Zhang is the Catherine M. and James E. Allchin Early Career Associate Professor in the School of Computer Science at Georgia Institute of Technology. He earned his Ph.D. in Computer Science and Engineering from The Chinese University of Hong Kong (2013) and bachelor's degree in Computer Science from Zhejiang University (2009). Zhang teaches graduate courses in compilers, software analysis, and program analysis, including CS 6340 Software Analysis and Test (Fall 2024) and CS 4240 Compilers and Interpreters (Spring 2025). His research focuses on improving software reliability and security through program analysis and compiler optimization techniques. Key research areas include computational complexity, analytic combinatorics, graph theory, and formal languages. Current projects include SLOT (SMT-LLVM Optimizing Translation) , Mutual Refinements of Context-Free Language Reachability , and Context-Free Language Reachability with Transitive Redundancy Elimination , among others. Zhang's research has produced award-winning work including the SIGSOFT Distinguished Paper Award (FSE 2023) and PLDI Distinguished Paper Award (2020). He has advised multiple students including Ph.D. graduates Shuo Ding (2024) and Yuanbo Li (now at Facebook), with Benjamin Mikek and Camille Bossut currently pursuing their Ph.D.s. As an academic leader, Zhang has served as: Artifacts Chair: PLDI'26, PLDI'25 Program Committee: PLDI'26, POPL'26, SAS'25, ASPLOS'25, SAS'24, FSE'24 External Reviewer: PLDI'19, PLDI'18 His group maintains active GitHub repositories for tools like Perses (syntax-guided program reduction) and Skeletal Program Enumeration (compiler testing framework). Zhang also contributes to educational resources by maintaining course materials on static analysis, symbolic execution, and webassembly analysis.

• Programming Languages
• Reversible Computing
• Software Systems
• +۲ مورد دیگر

Robert Glück is a Professor at the Department of Computer Science under the Faculty of Science , University of Copenhagen. He also served as a Visiting Professor at the National Institute of Informatics, Tokyo . His research spans programming languages , reversible computing , and metaprogramming , with a focus on energy-efficient computation. Email: glueck@di.ku.dk Phone: +45 29611655 Address: Universitetsparken 5, Building B, 2100 Copenhagen Ø Glück's research interests center on reversible computing , program generation , and metaprogramming , particularly for low-energy systems. His work includes developing reversible logic circuits, invertible interpreters, and tools for program inversion via term rewriting systems. Recent publications highlight advancements in reversible flowchart languages , partial evaluation techniques , and compiler design . Key themes include garbage-free reversibility, memory-efficient algorithms, and formal verification of reversible systems. Scientific Awards: Japan Society for the Promotion of Science (JSPS) Fellowship Grants & Projects: Presto Basic Research Grant (JST) Danish Council for Strategic Research (DSF) project Danish Council for Independent Research (FNU) project Administrative Roles: Current member of the Study Board for Mathematics and Computer Science Former Head of Studies for the Master in Computer Science Professional Activities: IFIP Technical Committee WG 2.11 member (2004–) Steering Committee roles at LOPSTR 2024, FLOPS 2024, HCVS 2024, RC 2024 Editorial Board member for New Generation Computing (2005–)