| l4_capfpage_struct_t | L4 Capability flexpage structure |
| l4_fpage_struct_t | L4 flexpage structure |
| l4_fpage_t | L4 flexpage type |
| l4_intrid_struct_t | L4 interrupt id structure |
| l4_intrid_t | L4 interrupt id |
| l4_iofpage_struct_t | L4 I/O flexpage structure |
| l4_ipc_deceit_ids_t | Structure used to describe destination and true source if a chief wants to deceit |
| l4_kernel_info_mem_desc_t | Memory descriptor data structure |
| l4_kernel_info_t | L4 Kernel Info Page |
| l4_low_high_t | 64 Bit -> 32 Bit low/high conversion |
| l4_msg_t | Structure to describe long IPC |
| l4_msgdope_struct_t | L4 message dope structure |
| l4_msgdope_t | L4 message dope type |
| l4_msgtag_t | Message tag for IPC operations |
| l4_quota_desc_t | Quota type structure |
| l4_sched_param_struct_t | Scheduling parameter structure |
| l4_sched_param_t | Scheduling parameter type |
| l4_snd_fpage_t | Send flexpage types |
| l4_strdope_t | L4 string dope |
| l4_threadid_struct_t | L4 thread id structure |
| l4_threadid_t | L4 thread id |
| l4_timeout_s | Basic timeout specification |
| l4_timeout_t | For IPC there are usually a send and a receive timeout |
| l4_tracebuffer_status_t | Tracebuffer status |
| l4_utcb_ex_regs_args | UTCB structure for l4_thread_ex_regs arguments |
| l4_utcb_exception | UTCB structure for exceptions |
| l4_utcb_t | UTCB |
| l4_utcb_task_new_args | UTCB structure for l4_task_new arguments |
| l4_vhw_descriptor | Virtual hardware devices description |
| l4_vhw_entry | Description of a device |