The view from the left
From MaRDI portal
Recommendations
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)