Feedback
Follow Us
Publication

Well-behaved (Co)algebraic semantics of regular expressions in Dafny

By Stefan Zetzsche, Wojciech Rozowski
2024
Download Copy BibTeX
Share
Download
Copy BibTeX
Share
Regular expressions are commonly understood in terms of their denotational semantics, that is, through formal languages – the regular languages. This view is inductive in nature: two primitives are equivalent if they are constructed in the same way. Alternatively, regular expressions can be understood in terms of their operational semantics, that is, through deterministic finite automata. This view is coinductive in nature: two primitives are equivalent if they are deconstructed in the same way. It is implied by Kleene’s famous theorem that both views are equivalent: regular languages are precisely the formal languages accepted by deterministic finite automata. In this paper, we use Dafny, a verification-aware programming language, to formally verify, for the first time, what has been previously established only through proofs-by-hand: the two semantics of regular expressions are well-behaved, in the sense that they are in fact one and the same, up to pointwise bisimiliarity. At each step of our formalisation, we propose an interpretation in the language of Coalgebra. We found that Dafny is particularly well suited for the task due to its inductive and coinductive features and hope our approach serves as a blueprint for future generalisations to other theories.
Research areas

Latest news

Work with us

See more jobs See more jobs
Applied Scientist, People eXperience and Technology Central Science Team (PXTCS)
CA, ON, Toronto
Are you motivated to explore research in ambiguous spaces? Are you interested in conducting research that will improve associate, employee and manager experiences at Amazon? Do you want to work on an interdisciplinary team of scientists that collaborate rather than compete? Join us at PXT Central Science! The People eXperience and Technology Central Science Team (PXTCS) uses economics, behavioral science, statistics, and machine learning to proactively identify mechanisms and process improvements which simultaneously improve Amazon and the lives, wellbeing, and the value of work to Amazonians. We are an interdisciplinary team that combines the talents of science and engineering to develop and deliver solutions that measurably achieve this goal. Key job responsibilities As an Applied Scientist for People Experience and Technology (PXT) Central Science, you will be working with our science and engineering teams, specifically on re-imagining Generative AI Applications and Generative AI Infrastructure for HR. Applying Generative AI to HR has unique challenges such as privacy, fairness, and seamlessly integrating Enterprise Knowledge and World Knowledge and knowing which to use when. In addition, the team works on some of Amazon’s most strategic technical investments in the people space and support Amazon’s efforts to be Earth’s Best Employer. In this role you will have a significant impact on 1.5 million Amazonians and the communities Amazon serves and ample scope to demonstrate scientific thought leadership and scientific impact in addition to business impact. You will also play a critical role in the organization's business planning, work closely with senior leaders to develop goals and resource requirements, influence our long-term technical and business strategy, and help hire and develop science and engineering talent. You will also provide support to business partners, helping them use the best scientific methods and science-driven tools to solve current and upcoming challenges and deliver efficiency gains in a changing marke About the team The AI/ML team in PXTCS is working on building Generative AI solutions to reimagine Corp employee and Ops associate experience. Examples of state-of-the-art solutions are Coaching for Amazon employees (available on AZA) and reinventing Employee Recruiting and Employee Listening.
Applied Scientist, International Machine Learning
IN, KA, Bengaluru
Do you want to join an innovative team of scientists who use machine learning and statistical techniques to create state-of-the-art solutions for providing better value to Amazon’s customers? Do you want to build and deploy advanced algorithmic systems that help optimize millions of transactions every day? Are you excited by the prospect of analyzing and modeling terabytes of data to solve real world problems? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you like to innovate and simplify? If yes, then you may be a great fit to join the Machine Learning and Data Sciences team for India Consumer Businesses. If you have an entrepreneurial spirit, know how to deliver, love to work with data, are deeply technical, highly innovative and long for the opportunity to build solutions to challenging problems that directly impact the company's bottom-line, we want to talk to you. Major responsibilities - Use machine learning and analytical techniques to create scalable solutions for business problems - Analyze and extract relevant information from large amounts of Amazon’s historical business data to help automate and optimize key processes - Design, development, evaluate and deploy innovative and highly scalable models for predictive learning - Research and implement novel machine learning and statistical approaches - Work closely with software engineering teams to drive real-time model implementations and new feature creations - Work closely with business owners and operations staff to optimize various business operations - Establish scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation - Mentor other scientists and engineers in the use of ML techniques
Applied Scientist, Artificial General Intelligence
US, MA, Boston
The Artificial General Intelligence (AGI) team is looking for a passionate, talented, and inventive Applied Scientist with a strong deep learning background, to build industry-leading Generative Artificial Intelligence (GenAI) technology with Large Language Models (LLMs) and multimodal systems. Key job responsibilities As a Applied Scientist with the AGI team, you will work with talented peers to lead the development of novel algorithms and modeling techniques, to advance the state of the art with LLMs. Your work will directly impact our customers in the form of products and services that make use of speech and language technology. You will leverage Amazon’s heterogeneous data sources and large-scale computing resources to accelerate advances in spoken language understanding. About the team The AGI team has a mission to push the envelope in GenAI with LLMs and multimodal systems, in order to provide the best-possible experience for our customers.
Economist, Amazon
US, WA, Seattle
The Global Cross-Channel and Cross- Category Marketing (XCM) org are seeking an experienced Economist to join our team. XCM’s mission is to be the most measurably effective and creatively breakthrough marketing organization in the world in order to strengthen the brand, grow the business, and reduce cost for Amazon overall. We achieve this through scaled campaigning in support of brands, categories, and audiences which aim to create the maximum incremental impact for Amazon as a whole by driving the Amazon flywheel. This is a high impact role with the opportunities to lead the development of state-of-the-art, scalable models to measure the efficacy and effectiveness of a new marketing channel. In this critical role, you will leverage your deep expertise in causal inference to design and implement robust measurement frameworks that provide actionable insights to drive strategic business decisions. Key Responsibilities: Develop advanced econometric and statistical models to rigorously evaluate the causal incremental impact of marketing campaigns on customer perception and customer behaviors. Collaborate cross-functionally with marketing, product, data science and engineering teams to define the measurement strategy and ensure alignment on objectives. Leverage large, complex datasets to uncover hidden patterns and trends, extracting meaningful insights that inform marketing optimization and investment decisions. Work with engineers, applied scientists and product managers to automate the model in production environment. Stay up-to-date with the latest research and methodological advancements in causal inference, causal ML and experiment design to continuously enhance the team's capabilities. Effectively communicate analysis findings, recommendations, and their business implications to key stakeholders, including senior leadership. Mentor and guide junior economists, fostering a culture of analytical excellence and innovation.
Applied Scientist, Amazon
US, WA, Seattle
The XCM (Cross Channel Cross-Category Marketing) team seeks an Applied Scientist to revolutionize our marketing strategies. XCM's mission is to build the most measurably effective, creatively impactful, and cross-channel campaigning capabilities possible, with the aim of growing "big-bet" programs, strengthening positive brand perceptions, and increasing long-term free cash flow. As a science team, we're tackling complex challenges in marketing incrementality measurement, optimization and audience segmentation. In this role, you'll collaborate with a diverse team of scientists and economists to build and enhance causal measurement, optimization and prediction models for Amazon's global multi-billion dollar fixed marketing budget. You'll also work closely with various teams to develop scientific roadmaps, drive innovation, and influence key resource allocation decisions. Key job responsibilities 1) Innovating scalable marketing methodologies using causal inference and machine learning. 2) Developing interpretable models that provide actionable business insights. 3) Collaborating with engineers to automate and scale scientific solutions. 4) Engaging with stakeholders to ensure effective adoption of scientific products. 5) Presenting findings to the Amazon Science community to promote excellence and knowledge-sharing.
Applied Scientist I, BRP (Buyer Risk Prevention)
US, WA, Seattle
Do you want to join an innovative team of scientists who use machine learning and statistical techniques to help Amazon provide the best customer experience by preventing eCommerce fraud? Are you excited by the prospect of analyzing and modeling terabytes of data and creating state-of-the-art algorithms to solve real world problems? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you enjoy collaborating in a diverse team environment? If yes, then you may be a great fit to join the Amazon Buyer Risk Prevention (BRP) Machine Learning group. We are looking for a talented scientist who is passionate to build advanced algorithmic systems that help manage safety of millions of transactions every day. Key job responsibilities Use machine learning and statistical techniques to create scalable risk management systems Learning and understanding large amounts of Amazon’s historical business data for specific instances of risk or broader risk trends Design, development and evaluation of highly innovative models for risk management Working closely with software engineering teams to drive real-time model implementations and new feature creations Working closely with operations staff to optimize risk management operations, Establishing scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation Tracking general business activity and providing clear, compelling management reporting on a regular basis Research and implement novel machine learning and statistical approaches
Applied Scientist I, BRP (Buyer Risk Prevention)
US, CA, San Diego
Do you want to join an innovative team of scientists who use machine learning and statistical techniques to help Amazon provide the best customer experience by preventing eCommerce fraud? Are you excited by the prospect of analyzing and modeling terabytes of data and creating state-of-the-art algorithms to solve real world problems? Do you like to own end-to-end business problems/metrics and directly impact the profitability of the company? Do you enjoy collaborating in a diverse team environment? If yes, then you may be a great fit to join the Amazon Buyer Risk Prevention (BRP) Machine Learning group. We are looking for a talented scientist who is passionate to build advanced algorithmic systems that help manage safety of millions of transactions every day. Key job responsibilities Use machine learning and statistical techniques to create scalable risk management systems Learning and understanding large amounts of Amazon’s historical business data for specific instances of risk or broader risk trends Design, development and evaluation of highly innovative models for risk management Working closely with software engineering teams to drive real-time model implementations and new feature creations Working closely with operations staff to optimize risk management operations, Establishing scalable, efficient, automated processes for large scale data analyses, model development, model validation and model implementation Tracking general business activity and providing clear, compelling management reporting on a regular basis Research and implement novel machine learning and statistical approaches
Applied Scientist, Conversational AI ModEling and Learning
CA, ON, Toronto
Conversational AI ModEling and Learning (CAMEL) team is part of Amazon Devices organization where our mission is to build a best-in-class Conversational AI that is intuitive, intelligent, and responsive, by developing superior Large Language Models (LLM) solutions and services which increase the capabilities built into the model and which enable utilizing thousands of APIs and external knowledge sources to provide the best experience for each request across millions of customers and endpoints. We are looking for a passionate, talented, and resourceful Applied Scientist in the field of LLM, Artificial Intelligence (AI), Natural Language Processing (NLP), Recommender Systems and/or Information Retrieval, to invent and build scalable solutions for a state-of-the-art context-aware conversational AI. A successful candidate will have strong machine learning background and a desire to push the envelope in one or more of the above areas. The ideal candidate would also have hands-on experiences in building Generative AI solutions with LLMs, enjoy operating in dynamic environments, be self-motivated to take on challenging problems to deliver big customer impact, moving fast to ship solutions and then iterating on user feedback and interactions. Key job responsibilities As an Applied Scientist, you will leverage your technical expertise and experience to collaborate with other talented applied scientists and engineers to research and develop novel algorithms and modeling techniques to reduce friction and enable natural and contextual conversations. You will analyze, understand and improve user experiences by leveraging Amazon’s heterogeneous data sources and large-scale computing resources to accelerate advances in artificial intelligence. You will work on core LLM technologies, including Prompt Engineering and Optimization, Supervised Fine-Tuning, Learning from Human Feedback, Evaluation, Self-Learning, etc. Your work will directly impact our customers in the form of novel products and services.
Applied Scientist, Conversational AI ModEling and Learning
CA, ON, Toronto
Conversational AI ModEling and Learning (CAMEL) team is part of Amazon Devices organization where our mission is to build a best-in-class Conversational AI that is intuitive, intelligent, and responsive, by developing superior Large Language Models (LLM) solutions and services which increase the capabilities built into the model and which enable utilizing thousands of APIs and external knowledge sources to provide the best experience for each request across millions of customers and endpoints. We are looking for a passionate, talented, and resourceful Applied Scientist in the field of LLM, Artificial Intelligence (AI), Natural Language Processing (NLP), Recommender Systems and/or Information Retrieval, to invent and build scalable solutions for a state-of-the-art context-aware conversational AI. A successful candidate will have strong machine learning background and a desire to push the envelope in one or more of the above areas. The ideal candidate would also have hands-on experiences in building Generative AI solutions with LLMs, enjoy operating in dynamic environments, be self-motivated to take on challenging problems to deliver big customer impact, moving fast to ship solutions and then iterating on user feedback and interactions. Key job responsibilities As an Applied Scientist, you will leverage your technical expertise and experience to collaborate with other talented applied scientists and engineers to research and develop novel algorithms and modeling techniques to reduce friction and enable natural and contextual conversations. You will analyze, understand and improve user experiences by leveraging Amazon’s heterogeneous data sources and large-scale computing resources to accelerate advances in artificial intelligence. You will work on core LLM technologies, including Prompt Engineering and Optimization, Supervised Fine-Tuning, Learning from Human Feedback, Evaluation, Self-Learning, etc. Your work will directly impact our customers in the form of novel products and services.
Data Scientist, EPP Analytics
US, WA, Seattle
We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA Do you love using data to solve complex problems? Are you interested in innovating and developing world-class big data solutions? We have the career for you! EPP Analytics team is seeking an exceptional Data Scientist to recommend, design and deliver new advanced analytics and science innovations end-to-end partnering closely with our security/software engineers, and response investigators. Your work enables faster data-driven decision making for Preventive and Response teams by providing them with data management tools, actionable insights, and an easy-to-use reporting experience. The ideal candidate will be passionate about working with big data sets and have the expertise to utilize these data sets to derive insights, drive science roadmap and foster growth. Key job responsibilities - As a Data Scientist (DS) in EPP Analytics, you will do causal data science, build predictive models, conduct simulations, create visualizations, and influence data science practice across the organization. - Provide insights by analyzing historical data - Create experiments and prototype implementations of new learning algorithms and prediction techniques. - Research and build machine learning algorithms that improve Insider Threat risk A day in the life No two days are the same in Insider Risk teams - the nature of the work we do and constantly shifting threat landscape means sometimes you'll be working with an internal service team to find anomalous use of their data, other days you'll be working with IT teams to build improved controls. Some days you'll be busy writing detections, or mentoring or running design review meetings. The EPP Analytics team is made up of SDEs and Security Engineers who partner with Data Scientists to create big data solutions and continue to raise the bar for the EPP organization. As a member of the team you will have the opportunity to work on challenging data modeling solutions, new and innovative Quicksight based reporting, and data pipeline and process improvement projects. About the team Diverse Experiences Amazon Security values diverse experiences. Even if you do not meet all of the qualifications and skills listed in the job description, we encourage candidates to apply. If your career is just starting, hasn’t followed a traditional path, or includes alternative experiences, don’t let it stop you from applying. Why Amazon Security? At Amazon, security is central to maintaining customer trust and delivering delightful customer experiences. Our organization is responsible for creating and maintaining a high bar for security across all of Amazon’s products and services. We offer talented security professionals the chance to accelerate their careers with opportunities to build experience in a wide variety of areas including cloud, devices, retail, entertainment, healthcare, operations, and physical stores Inclusive Team Culture In Amazon Security, it’s in our nature to learn and be curious. Ongoing DEI events and learning experiences inspire us to continue learning and to embrace our uniqueness. Addressing the toughest security challenges requires that we seek out and celebrate a diversity of ideas, perspectives, and voices. Training & Career Growth We’re continuously raising our performance bar as we strive to become Earth’s Best Employer. That’s why you’ll find endless knowledge-sharing, training, and other career-advancing resources here to help you develop into a better-rounded professional. Work/Life Balance We value work-life harmony. Achieving success at work should never come at the expense of sacrifices at home, which is why flexible work hours and arrangements are part of our culture. When we feel supported in the workplace and at home, there’s nothing we can’t achieve.
View from space of a connected network around planet Earth representing the Internet of Things.
Have feedback?
Let us know by taking this short survey
Get started

Amazon.com | Conditions of Use | Privacy | © 1996-2024 Amazon.com, Inc. or its affiliates

Follow Us