Verifying haskell programs using constructive type theory

No abstract is available for this paper.

• Publication year

  2005

• Venue

  ACM SIGPLAN Symposium/Workshop on Haskell

• Publication date

  2005-09-30

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1088348.1088355
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• General recursion via coinductive types

  2005influential reference
• The logic of demand in Haskell

  2005influential reference
• An Overview of the Programatica Toolset

  2004cited by this paper
• Reasoning About CBV Functional Programs in Isabelle / HOL ? ? ?

  2004influential reference
• Interactive Theorem Proving and Program Development

  2004influential reference
• Verification of non-functional programs using interpretations in type theory

  2003cited by this paper
• Theorem Proving for Functional Programmers

  2002influential reference
• Implementation of Functional Languages: 13th International Workshop, IFL 2001 Stockholm, Sweden, September 24-26, 2001 Selected Papers

  2002cited by this paper
• Monad Translating Inductive and Coinductive Types

  2002cited by this paper
• QuickCheck: a lightweight tool for random testing of Haskell programs

  2000influential reference
• System Description: Twelf - A Meta-Logical Framework for Deductive Systems

  1999cited by this paper
• Monadic Type Systems: Pure Type Systems for Impure Settings

  1998influential reference
• Formal Reasoning about Communication Systems I: Embedding ML into Type Theory.

  1997cited by this paper
• Finitely Stratified Polymorphism

  1991cited by this paper
• How to make ad-hoc polymorphism less ad hoc

  1989cited by this paper
• The Calculus of Constructions

  1988cited by this paper
• Intuitionistic type theory

  1984cited by this paper
• The formulae-as-types notion of construction

  1969cited by this paper
• Under Consideration for Publication in J. Functional Programming Building Reliable, High-performance Networks with the Nuprl Proof Development System

  year unknowncited by this paper

• Pinpointing the Learning Obstacles of an Interactive Theorem Prover

  2025cites this paper
• A model of Solidity-style smart contracts in the theorem prover Agda

  2023cites this paper
• Reasonable Agda is correct Haskell: writing verified Haskell using agda2hs

  2022cites this paper
• An approach to translating Haskell programs to Agda and reasoning about them

  2022cites this paper
• Regularity and quantification: a new approach to verify distributed protocols

  2022cites this paper
• A Monadic Implementation of Functional Logic Programs

  2022cites this paper
• Reasoning about the garden of forking paths

  2021cites this paper
• Haskell⁻¹: automatic function inversion in Haskell

  2021cites this paper
• Modular verification of programs with effects and effects handlers

  2020cites this paper
• Effectful Programming in Declarative Languages with an Emphasis on Non-Determinism: Applications and Formal Reasoning

  2020influential citation
• Verifying effectful Haskell programs in Coq

  2019influential citation
• Generic and flexible defaults for verified, law-abiding type-class instances

  2019cites this paper
• One Monad to Prove Them All (Functional Pearl)

  2018cites this paper
• Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)

  2018cites this paper
• Total Haskell is reasonable Coq

  2017cites this paper
• 2 The Concept of Explicit Strictness

  2017influential citation
• P roof Tool Support for E xplicit Strictness

  2017influential citation
• Using Coq to write fast and correct Haskell

  2017cites this paper
• Theorem Provers as Libraries - An Approach to Formally Verifying Functional Programs

  2015influential citation
• Static Contract Checking via First-Order Logic

  2014cites this paper
• Certified HLints with Isabelle/HOLCF-Prelude

  2013cites this paper
• HeisenBase : Understanding Database Performance in Haskell Dept . of CIS-Senior Design 2012-2013

  2013influential citation
• HaskHOL: A Haskell Hosted Domain Specific Language for Higher-Order Logic Theorem Proving

  2011cites this paper
• Verification of SequenceL programs using Mizar

  2010cites this paper
• Embedding a logical theory of constructions in Agda

  2009cites this paper
• Verification of Parametric Counter Automata in a Dependently Typed Language

  2009cites this paper
• Proving Properties of Lazy Functional Programs with Sparkle

  2008influential citation
• A Hoare Logic for Call-by-Value Functional Programs

  2008cites this paper
• Monads through program extraction

  2008cites this paper
• Implementation of a Pragmatic Translation from Haskell into Isabelle / HOL

  2008cites this paper
• A coinductive monad for prop-bounded recursion

  2007cites this paper
• 2 Semantic Background of the Translation

  2007cites this paper
• Theorem Proving in Higher Order Logics and Applications -- Emerging Trends

  2007cites this paper
• Selective strictness and parametricity in structural operational semantics, inequationally

  2007cites this paper
• Extended Static Checking of Call-by-Value Functional Programs

  2007cites this paper
• Formalising a High-Performance Microkernel Kevin Elphinstone Gerwin

  2006cites this paper
• Formalising a High-Performance Microkernel Kevin Elphinstone Gerwin

  2006cites this paper
• Running the manual: an approach to high-assurance microkernel development

  2006cites this paper
• Formalising a high-performance microkernel

  2006cites this paper
• Verification of an Optimisation Algorithm of Stack Machine in Functional Programming Languages

  2006cites this paper
• Proof Tool Support for Explicit Strictness

  2005influential citation