We provide a logical system to express Minimalist Grammars, whichaims at being ``minimal'' in the sense that it contains the least rulesand the simplest lexical entries possible. By limiting ourselves to theproofs that satisfy a constraint on hypothesis management, we simulateminimalist derivations. This system is an elaboration of previous workby Lecomte and Retoré which were based on a new use of the Lambekcalculus, where words were no longer associated with formulae, but withaxioms, and where a proof of a sentence was a proof of the theorem $$ \vdash c$$ instead of a proof of a sequent $$\Gamma \vdash c$$ . Such a calculus which suffered from limitations is herereplaced by a version of partially non-commutative linear logic, due toP. de Groote, and we show that in this system, when we limit ourselvesto special proofs, we may mimic move (besides of coursemerge) for A-movement as well as head-movement. Moreover weshow that the use of second-order types, allowed by the categorialgrammar tradition, brings solutions for linguistic problems, includingexpletives and unbounded dependencies. We think that such a system islegitimated by its strong logical foundation, the fact that complexityresults can be derived and also by philosophical reasons, which arelinked to the way we may conceive logics: not only as aformalisation of reasoning but as a theory of generalobjects.