The view from the left
From MaRDI portal
Recommendations
Cited in
(42)- Strongly typed term representations in Coq
- Recursive coalgebras from comonads
- Containers: Constructing strictly positive types
- Proofs for free. Parametricity for dependent types
- Constructive membership predicates as index types
- Let's see how things unfold: reconciling the infinite with the intensional (extended abstract)
- A unified treatment of syntax with binders
- Algebra of Programming Using Dependent Types
- Structural subtyping for inductive types with functorial equality rules
- Modular development of certified program verifiers with a proof assistant,
- Hoare type theory, polymorphism and separation
- Pattern matching with abstract data types
- A New Elimination Rule for the Calculus of Inductive Constructions
- Big-step normalisation
- Algebra of programming in Agda: Dependent types for relational program derivation
- Dependently typed programming in Agda
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Elaborating dependent (co)pattern matching: no pattern left behind
- Eliminating dependent pattern matching without K
- Programming with ornaments
- Interactive programming in Agda -- objects and graphical user interfaces
- Idris, a general-purpose dependently typed programming language: Design and implementation
- A library for polymorphic dynamic typing
- The Implicit Calculus of Constructions as a Programming Language with Dependent Types
- Partiality and recursion in interactive theorem provers -- an overview
- Equations: a dependent pattern-matching compiler
- Eliminating Dependent Pattern Matching
- Propositional forms of judgemental interpretations
- Calculating datastructures
- Trace-based verification of imperative programs with I/O
- Coalgebras in functional programming and type theory
- Builtin types viewed as inductive families
- Correct and complete type checking and certified erasure for \textsc{Coq}, in \textsc{Coq}
- Deep induction for inductive families
- Call-by-value and call-by-name: a simple proof of a classic theorem
- A practical formalization of monadic equational reasoning in dependent-type theory
- A lambda term representation inspired by linear ordered logic
- Sequent calculus and equational programming
- Dependently typed array programs don't go wrong
- A principled approach to programming with nested types in Haskell
- 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)
