Roughly speaking, in set forcing the forcing notion is a set from ground model's perspective and in class forcing its a definable subset of the ground model given by solutions of some formula with parameters. But in a model theoretic point of view we can go further from definability with single formulas and define type-definable subsets of a given model which are given by solutions of a consistent (and infinite) set of formulas which uses only finite number of parameters from ground model. It is somehow like considering definability over a ground model in an infinitary logic which allows using $\omega$-many conjunctions.
Of course we need some restrictions and conditions on class forcing to make it $ZFC$-preserving. i.e. To be sure that the generic extension of a model of $ZFC$ remains a model of $ZFC$.
Question: Is there any reference for forcing theory in a non-first order setting including infinitary or higher order logics? What should be the conditions for making type-definable forcing $ZFC$-preserving?