Is it possible to implement this? Yes. (Well it is possible to implement in any programming language, but Mathematica is actually a good choice, which is what really matters). Mathematica/The Wolfram Language excels at describing symbolic transformations and typsetting different notations. But what features are you looking for? If you look online a bit, it looks like there's implementations in COQ, which would be useful for theorem proving. I don't know what you intend to do. 

The first thing to do is to implement sequent calculus using ordinary expressions. After that, you can use the Notation package in Mathematica to create the kind of typesetting you want. To begin with, I'd read thru the Mathematica virtual book to get a feeling for how to program in Mathematica. After that, take a look at the Notation package in the documentation.