The following pages link to The view from the left (Q4819653):
Displayed 32 items.
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Dependently typed array programs don't go wrong (Q843222) (← links)
- A principled approach to programming with nested types in Haskell (Q848745) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Strongly typed term representations in Coq (Q2392480) (← links)
- Recursive coalgebras from comonads (Q2495640) (← links)
- Containers: Constructing strictly positive types (Q2566024) (← links)
- Proofs for free (Q2844694) (← links)
- Constructive Membership Predicates as Index Types (Q2866329) (← links)
- Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract) (Q2888481) (← links)
- A unified treatment of syntax with binders (Q3165528) (← links)
- Algebra of Programming Using Dependent Types (Q3521992) (← links)
- Structural subtyping for inductive types with functorial equality rules (Q3535679) (← links)
- Modular development of certified program verifiers with a proof assistant, (Q3546045) (← links)
- Hoare type theory, polymorphism and separation (Q3546051) (← links)
- A New Elimination Rule for the Calculus of Inductive Constructions (Q3638245) (← links)
- Big-step normalisation (Q3638919) (← links)
- Algebra of programming in Agda: Dependent types for relational program derivation (Q3644935) (← links)
- Dependently Typed Programming in Agda (Q3649136) (← links)
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know (Q4912883) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- Elaborating dependent (co)pattern matching: No pattern left behind (Q5110925) (← links)
- Eliminating dependent pattern matching without K (Q5371975) (← links)
- Programming with ornaments (Q5372000) (← links)
- Interactive programming in Agda – Objects and graphical user interfaces (Q5372002) (← links)
- Idris, a general-purpose dependently typed programming language: Design and implementation (Q5398331) (← links)
- A library for polymorphic dynamic typing (Q5398333) (← links)
- The Implicit Calculus of Constructions as a Programming Language with Dependent Types (Q5458373) (← links)
- Partiality and recursion in interactive theorem provers – an overview (Q5741556) (← links)
- Propositional forms of judgemental interpretations (Q6053842) (← links)
- Calculating datastructures (Q6109206) (← links)