This special issue of Logical Methods in Computer Science (LMCS) is devoted to the recent progress in the technology of formal methods: notably the design and verification of software, hardware, and mathematics based on type theory. It continues the tradition originated by several books published by Springer under the same title since 1993. The issue consists of nine articles selected out of 22 submissions resulting from an open call for papers circulated in the Types community. These papers cover various aspects of constructive type theory and its applications, in particular formalizing mathematics and issues related to proof-assistants and proof technology. Papers on the following topics are included:

As to 1, Denis Cousineau's paper "On completeness of reducibility candidates as a semantics of strong normalization" provides a semantical characterization of the strong normalization property for theories in deduction modulo a la Curry: a theory is strongly normalizing iff it admits a certain model.
Then Pablo Arrighi and Alejandro Daz-Caro wrote "A System F accounting for scalars", which studies a variant of polymorphic type assignment (system F) to the linear algebraic lambda-calculus, where linear combinations of lambda-terms are possible.
With "On streams that are finitely red" Marc Bezem, Keiko Nakata, and Tarmo Uustalu study constructive definitions of the notion of finiteness, in particular relations between various constructive interpretations of the quantifier "almost every".
As to 2, in the paper of James Cheney "A dependent nominal type theory", an LF-style dependent type theory is proposed which provides a type-theoretic framework for the nominal approach to abstract syntax.
Then "On Irrelevance and Algorithmic Equality in Predicative Type Theory", by Andreas Abel and Gabriel Scherer, proposes a type theory for dependently typed programs, extending the Martin-Lof type theory by so called irrelevant quantifiers (another form of dependent product). The motivation for this work is eliminating computationally irrelevant code at compile time.
As to 3, in "A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving", by Freek Wiedijk, a new generic approach is proposed to combine the procedural and declarative styles of interactive theorem proving. The method is fully implemented as a proof interface miz3.
In "A bi-directional refinement algorithm for the calculus of (co)inductive constructions" Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi describe a type inference algorithm for the Calculus of Inductive Constructions, as implemented in the Matita theorem prover.
As to 4, in "Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination", Assia Mahboubi and Cyril Cohen provide a formalization in Coq of the theory of discrete real closed fields, which captures in particular a computational formalization of algebraic numbers.
Finally Thomas Braibant and Damien Pous provide with their paper "Deciding Kleene Algebras in Coq" a high-level Coq tactic to decide equations in Kleene algebras, thus making progress in developing tools to handle binary relations in Coq.
The craftmanship of turning mathematics into lambda terms as formal proofs has been developing impressively in the period 1970-2012. In 1970 the first (not yet interactive) systems of Automath by N.G. de Bruijn and collaborators started to be used for formalization (and hence checking). During the last decade highly non trivial mathematical formalization results have been established in type theory (system Coq): Four Colour Theorem (2005), Feit-Thompson theorem (2012), by Georges Gonthier and collaborators. In spite of the possibility of formalizing, the craftmanship to do so remains a time consuming skill. We hope that this issue eventually contributes to turning mathematics into formal proofs in a less labour consuming way.

The Editors wish to thank all authors for their submissions to this special issue, as well as all the anonymous reviewers.