The view from the left

DOI10.1017/S0956796803004829MaRDI QIDQ4819653zbMATH OpenOpenAlexWikidataFDO

Authors Conor McBride, James McKinna

Publication date 27 September 2004

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0956796803004829

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Pattern matching with abstract data types
• A typed pattern calculus
• Elaborating dependent (co)pattern matching: no pattern left behind
• Pattern matching without K
• A New Elimination Rule for the Calculus of Inductive Constructions

Cited in

(36)

• Recursive coalgebras from comonads
• Modular development of certified program verifiers with a proof assistant,
• Constructive membership predicates as index types
• Big-step normalisation
• Equations: a dependent pattern-matching compiler
• A New Elimination Rule for the Calculus of Inductive Constructions
• Proofs for free. Parametricity for dependent types
• A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
• Eliminating dependent pattern matching without K
• Structural subtyping for inductive types with functorial equality rules
• Interactive programming in Agda -- objects and graphical user interfaces
• Dependently typed programming in Agda
• Algebra of programming in Agda: Dependent types for relational program derivation
• Trace-based verification of imperative programs with I/O
• Containers: Constructing strictly positive types
• Calculating datastructures
• Builtin types viewed as inductive families
• Algebra of Programming Using Dependent Types
• Propositional forms of judgemental interpretations
• Strongly typed term representations in Coq
• Elaborating dependent (co)pattern matching: no pattern left behind
• A principled approach to programming with nested types in Haskell
• Eliminating Dependent Pattern Matching
• A library for polymorphic dynamic typing
• Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
• A unified treatment of syntax with binders
• Dependently typed array programs don't go wrong
• Partiality and recursion in interactive theorem provers -- an overview
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Programming with ornaments
• Pattern matching with abstract data types
• Hoare type theory, polymorphism and separation
• Coalgebras in functional programming and type theory
• An insider's look at LF type reconstruction: everything you (n)ever wanted to know
• The Implicit Calculus of Constructions as a Programming Language with Dependent Types
• A computer-verified monadic functional implementation of the integral

This page was built for publication: The view from the left

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4819653)