The view from the left
From MaRDI portal
Publication:4819653
DOI10.1017/S0956796803004829zbMath1069.68539OpenAlexW2062887328WikidataQ55980134 ScholiaQ55980134MaRDI QIDQ4819653
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
Related Items
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, A principled approach to programming with nested types in Haskell, Strongly typed term representations in Coq, Trace-based verification of imperative programs with I/O, Propositional forms of judgemental interpretations, Calculating datastructures, Elaborating dependent (co)pattern matching: No pattern left behind, Algebra of Programming Using Dependent Types, Coalgebras in functional programming and type theory, Eliminating dependent pattern matching without K, Programming with ornaments, Interactive programming in Agda – Objects and graphical user interfaces, 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, Idris, a general-purpose dependently typed programming language: Design and implementation, A library for polymorphic dynamic typing, An insider's look at LF type reconstruction: everything you (n)ever wanted to know, Partiality and recursion in interactive theorem provers – an overview, Recursive coalgebras from comonads, A computer-verified monadic functional implementation of the integral, The Implicit Calculus of Constructions as a Programming Language with Dependent 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, Proofs for free, Containers: Constructing strictly positive types, Constructive Membership Predicates as Index Types, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
