diff --git a/Papyrus/IR/InstructionRefs.lean b/Papyrus/IR/InstructionRefs.lean
index 2ac9104..90ae5a0 100644
--- a/Papyrus/IR/InstructionRefs.lean
+++ b/Papyrus/IR/InstructionRefs.lean
@@ -403,3 +403,77 @@ def createCall
   CallInstRef.create (← self.getFunctionType) self args name
 
 end FunctionRef
+
+--------------------------------------------------------------------------------
+-- # PHI
+--------------------------------------------------------------------------------
+
+/--
+  A reference to an external LLVM
+  [PHINode](https://llvm.org/doxygen/classllvm_1_1PHINode.html).
+-/
+structure PHINodeRef extends InstructionRef, ValueRef
+instance : Coe PHINodeRef InstructionRef := ⟨(·.toInstructionRef)⟩
+
+namespace PHINodeRef
+/-- Create a new phi node instruction. -/
+@[extern "papyrus_phi_node_create"]
+constant create (type : @& TypeRef) (numReservedValues : UInt32 := 0) (name : @& String := "") : IO PHINodeRef
+
+/-- Create a new phi node instruction at the end of a given basic block.  -/
+@[extern "papyrus_phi_node_create_at_end"]
+constant createAtEnd (type : @& TypeRef) (numReservedValues : UInt32 := 0) (name : @& String := "") (bb : @& BasicBlockRef) : IO PHINodeRef
+
+/-- Create a new phi node instruction after the given instruction.  -/
+@[extern "papyrus_phi_node_create_after"]
+constant createAfter (type : @& TypeRef) (numReservedValues : UInt32 := 0) (name : @& String := "") (inst : @& InstructionRef) : IO PHINodeRef
+
+/-- get incoming value number i  -/
+@[extern "papyrus_phi_node_get_incoming_value"]
+constant getIncomingValue! (node : @& PHINodeRef) (i : UInt32) : IO ValueRef
+
+/-- set incoming value number i -/
+@[extern "papyrus_phi_node_set_incoming_value"]
+constant setIncomingValue! (node : @& PHINodeRef) (i : UInt32) (value : @& ValueRef) : IO PUnit
+
+/-- get incoming block number i  -/
+@[extern "papyrus_phi_node_get_incoming_block"]
+constant getIncomingBlock! (node : @& PHINodeRef) (i : UInt32) : IO BasicBlockRef
+
+/-- set incoming block number i -/
+@[extern "papyrus_phi_node_set_incoming_block"]
+constant setIncomingBlock! (node : @& PHINodeRef) (i : UInt32) (value : @& BasicBlockRef) : IO PUnit
+
+/-- add an incoming value to the phi node list -/
+@[extern "papyrus_phi_node_add_incoming"]
+constant addIncoming (node : @& PHINodeRef) (value : @& ValueRef) (bb : @& BasicBlockRef) : IO PUnit
+
+/-- remove an incoming value to the phi node list -/
+@[extern "papyrus_phi_node_remove_incoming_value"]
+constant removeIncomingValue (node : @& PHINodeRef) (bb : @& BasicBlockRef) (deleteIfPHIEmpty : Bool := true) : IO ValueRef
+
+/-- get blocks branching to this phi node -/
+@[extern "papyrus_phi_node_get_blocks"]
+constant getBlocks (node : @& PHINodeRef) : IO (Array BasicBlockRef)
+
+/-- get incoming values to this phi node -/
+@[extern "papyrus_phi_node_incoming_values"]
+constant getValues (node : @& PHINodeRef) : IO (Array ValueRef)
+
+/-- set incoming value for block -/
+@[extern "papyrus_phi_node_set_incoming_value_for_block"]
+constant setIncomingValueForBlock (node : @& PHINodeRef) (bb : @& BasicBlockRef) (value : @& ValueRef) : IO PUnit
+
+/-- get incoming value for block -/
+@[extern "papyrus_phi_node_get_incoming_value_for_block"]
+constant getIncomingValueForBlock (node : @& PHINodeRef) (bb : @& BasicBlockRef) : IO ValueRef
+
+/-- whether all blocks have an incoming value -/
+@[extern "papyrus_phi_node_is_complete"]
+constant isComplete (node : @& PHINodeRef) : IO Bool
+
+/-- whether the phi node merges together the same value -/
+@[extern "papyrus_phi_node_has_constant_or_undef_value"]
+constant hasConstantOrUndefValue (node : @& PHINodeRef) : IO Bool
+
+end PHINodeRef
\ No newline at end of file
diff --git a/c/src/instruction.cpp b/c/src/instruction.cpp
index c61faf7..d093731 100644
--- a/c/src/instruction.cpp
+++ b/c/src/instruction.cpp
@@ -433,4 +433,138 @@ extern "C" lean_obj_res papyrus_call_inst_create
 	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
 }
 
+//------------------------------------------------------------------------------
+// PHI
+//------------------------------------------------------------------------------
+
+// Get the LLVM StoreInst pointer wrapped in an object.
+PHINode* toPHINode(lean_object* instRef) {
+	return llvm::cast<PHINode>(toValue(instRef));
+}
+
+// Get a reference to a newly created phi instruction.
+extern "C" lean_obj_res papyrus_phi_node_create
+	(b_lean_obj_res typeRef, unsigned numReservedValues, b_lean_obj_res nameObj, lean_obj_arg /* w */)
+{
+	auto i = PHINode::Create(toType(typeRef), numReservedValues, refOfString(nameObj));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
+}
+
+// Get a reference to a newly created phi instruction inserted at the end of the given basic block
+extern "C" lean_obj_res papyrus_phi_node_create_at_end
+	(b_lean_obj_res typeRef, unsigned numReservedValues, b_lean_obj_res nameObj, b_lean_obj_res bb, lean_obj_arg /* w */)
+{
+	auto i = PHINode::Create(toType(typeRef), numReservedValues, refOfString(nameObj), toBasicBlock(bb));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
+}
+
+// Get a reference to a newly created phi instruction inserted after the given instruction
+extern "C" lean_obj_res papyrus_phi_node_create_after
+	(b_lean_obj_res typeRef, unsigned numReservedValues, b_lean_obj_res nameObj, b_lean_obj_res inst, lean_obj_arg /* w */)
+{
+	auto i = PHINode::Create(toType(typeRef), numReservedValues, refOfString(nameObj), toInstruction(inst));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(typeRef), i));
+}
+
+// return incoming value number i
+extern "C" lean_obj_res papyrus_phi_node_get_incoming_value
+	(b_lean_obj_res instRef, unsigned i, lean_obj_arg /* w */)
+{
+	auto val = toPHINode(instRef)->getIncomingValue(i);
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), val));
+}
+
+// set incoming value number i
+extern "C" lean_obj_res papyrus_phi_node_set_incoming_value
+	(b_lean_obj_res instRef, unsigned i, b_lean_obj_res val, lean_obj_arg /* w */) {
+	toPHINode(instRef)->setIncomingValue(i, toValue(val));
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+// return incoming block number i
+extern "C" lean_obj_res papyrus_phi_node_get_incoming_block
+	(b_lean_obj_res instRef, unsigned i, lean_obj_arg /* w */)
+{
+	auto bb = toPHINode(instRef)->getIncomingBlock(i);
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), bb));
+}
+
+// set incoming block number i
+extern "C" lean_obj_res papyrus_phi_node_set_incoming_block
+	(b_lean_obj_res instRef, unsigned i, b_lean_obj_res val, lean_obj_arg /* w */) {
+	toPHINode(instRef)->setIncomingBlock(i, toBasicBlock(val));
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+// add an incoming value to the end of the PHI list
+extern "C" lean_obj_res papyrus_phi_node_add_incoming
+	(b_lean_obj_res instRef, b_lean_obj_res val, b_lean_obj_res bb, lean_obj_arg /* w */) {
+	toPHINode(instRef)->addIncoming(toValue(val), toBasicBlock(bb));
+	return lean_io_result_mk_ok(lean_box(0));
+} 
+
+// remove an incoming value for the given block
+extern "C" lean_obj_res papyrus_phi_node_remove_incoming_value
+	(b_lean_obj_res instRef,  b_lean_obj_res bb, uint8_t deleteIfPHIEmpty, lean_obj_arg /* w */) {
+	auto val = toPHINode(instRef)->removeIncomingValue(toBasicBlock(val), deleteIfPHIEmpty);
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), val));
+} 
+
+// get the array of blocks of this phi node
+extern "C" lean_obj_res papyrus_phi_node_blocks
+	(b_lean_obj_res instRef, lean_obj_arg /* w */) {
+	auto link = borrowLink(instRef);
+	auto blocks = toPHINode(instRef)->blocks();
+	lean_object* arr = lean_alloc_array(0, PAPYRUS_DEFAULT_ARRAY_CAPCITY);
+	for (auto& block : blocks) {
+		lean_inc_ref(link);
+		arr = lean_array_push(arr, mkValueRef(link, block));
+	}
+	return lean_io_result_mk_ok(arr);
+}
+
+// get array of incoming values for phi node
+extern "C" lean_obj_res papyrus_phi_node_incoming_values
+	(b_lean_obj_res instRef, lean_obj_arg /* w */) {
+
+	auto link = borrowLink(instRef);
+	auto values = toPHINode(instRef)->incoming_values();
+	lean_object* arr = lean_alloc_array(0, PAPYRUS_DEFAULT_ARRAY_CAPCITY);
+	for (auto& value : values) {
+		lean_inc_ref(link);
+		arr = lean_array_push(arr, mkValueRef(link, value.get()));
+	}
+	return lean_io_result_mk_ok(arr);
+}
+
+// set incoming value of block
+extern "C" lean_obj_res papyrus_phi_node_set_incoming_value_for_block
+	(b_lean_obj_res instRef, b_lean_obj_res bb, b_lean_obj_res val, lean_obj_arg /* w */) {
+	toPHINode(instRef)->setIncomingValueForBlock(toBasicBlock(bb), toValue(val));
+	return lean_io_result_mk_ok(lean_box(0));
+}
+
+// return incoming value for given block
+extern "C" lean_obj_res papyrus_phi_node_get_incoming_value_for_block
+	(b_lean_obj_res instRef, b_lean_obj_res bb, lean_obj_arg /* w */)
+{
+	auto val = toPHINode(instRef)->getIncomingValueForBlock(toBasicBlock(bb));
+	return lean_io_result_mk_ok(mkValueRef(copyLink(instRef), val));
+}
+
+// whether the phi node has incoming values for all predecessors 
+extern "C" uint8_t papyrus_phi_node_is_complete
+	(b_lean_obj_res instRef, lean_obj_arg /* w */)
+{
+	return toPHINode(instRef)->isComplete();
+}
+
+extern "C" uint8_t papyrus_phi_node_has_constant_or_undef_value
+	(b_lean_obj_res instRef, lean_obj_arg /* w */)
+{
+	return toPHINode(instRef)->hasConstantOrUndefValue();
+}
+
+
+
 } // end namespace papyrus
diff --git a/test/run/ir/instructionRefs.lean b/test/run/ir/instructionRefs.lean
index 35d05f0..7f42b53 100644
--- a/test/run/ir/instructionRefs.lean
+++ b/test/run/ir/instructionRefs.lean
@@ -129,3 +129,16 @@ def assertBEq [Repr α] [BEq α] (expected actual : α) : IO PUnit := do
   let inst ← CallInstRef.create fnTy fn #[]
   assertBEq ValueKind.instruction inst.valueKind
   assertBEq InstructionKind.call inst.instructionKind
+
+-- `PHI Node`
+#eval LlvmM.run do
+  let i8Ty ← int8Type.getRef -- type of the PHI Node
+  let then_ ← BasicBlockRef.create "then"
+  let else_ ← BasicBlockRef.create "else"
+  let merge_ ← BasicBlockRef.create "ifcont"
+  let inst ← CondBrInstRef.create then_ else_ (← ConstantIntRef.ofBool true)
+  let thenValue ← ConstantIntRef.ofUInt8 0
+  let elseValue ← ConstantIntRef.ofUInt8 2
+  let phi ← PHINodeRef.createAtEnd i8Ty (numReservedValues := 2) (name := "iftmp") (bb := merge_)
+  phi.addIncoming thenValue then_
+  phi.addIncoming elseValue else_
\ No newline at end of file